∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] [ExistsAddOfLE α]
  [inst_4 : AddCommMonoid β] [inst_5 : PartialOrder β] [IsOrderedCancelAddMonoid β] [inst_7 : Module α β]
  [PosSMulMono α β] {a₁ a₂ : α} {b₁ b₂ : β}, a₁ ≤ a₂ → b₁ ≤ b₂ → a₁ • b₂ + a₂ • b₁ ≤ a₁ • b₁ + a₂ • b₂