∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
  [inst_4 : Zero β],
  (∀ ⦃a : α⦄, 0 < a → ∀ ⦃b₁ b₂ : β⦄, b₁ < b₂ → a • b₁ < a • b₂) →
    (∀ ⦃b : β⦄, 0 < b → ∀ ⦃a₁ a₂ : α⦄, a₁ < a₂ → a₁ • b < a₂ • b) → IsStrictOrderedModule α β