Further lemmas about monotonicity of scalar multiplication

@[simp]

theorem abs_smul {α : Type u_1} {β : Type u_2} [Ring α] [LinearOrder α] [IsOrderedRing α] [AddCommGroup β] [LinearOrder β] [IsOrderedAddMonoid β] [Module α β] [PosSMulMono α β] (a : α) (b : β) : |a • b| = |a| • |b|