∀ {α : Type u_1} {b c : α} {K : Type u_2} [inst : Semiring K] [inst_1 : PartialOrder K] [inst_2 : AddCommMonoid α]
  [inst_3 : PartialOrder α] [inst_4 : Module K α] [PosSMulStrictMono K α], b < c → ∀ {s : K}, 0 < s → s • b < s • c