{α : Type u_1} →
  {β : Type u_2} →
    [inst : SMul α β] →
      [inst_1 : Preorder α] →
        [inst_2 : Preorder β] →
          [inst_3 : Zero α] →
            [inst_4 : Zero β] →
              {motive : IsStrictOrderedModule α β → Sort u} →
                (t : IsStrictOrderedModule α β) →
                  ([toPosSMulStrictMono : PosSMulStrictMono α β] →
                      [toSMulPosStrictMono : SMulPosStrictMono α β] → motive ⋯) →
                    motive t