Further lemmas about monotonicity of scalar multiplication

theorem inf_eq_half_smul_add_sub_abs_sub (R : Type u_2) {M : Type u_3} [Semiring R] [Invertible 2] [Lattice M] [AddCommGroup M] [Module R M] [IsOrderedAddMonoid M] (x y : M) : x ⊓ y = ⅟2 • (x + y - |y - x|)

theorem sup_eq_half_smul_add_add_abs_sub (R : Type u_2) {M : Type u_3} [Semiring R] [Invertible 2] [Lattice M] [AddCommGroup M] [Module R M] [IsOrderedAddMonoid M] (x y : M) : x ⊔ y = ⅟2 • (x + y + |y - x|)

@[simp]

theorem abs_smul {R : Type u_2} {M : Type u_3} [Ring R] [LinearOrder R] [IsOrderedRing R] [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module R M] [PosSMulMono R M] (a : R) (b : M) : |a • b| = |a| • |b|

theorem inf_eq_half_smul_add_sub_abs_sub' (𝕜 : Type u_1) {M : Type u_3} [DivisionSemiring 𝕜] [NeZero 2] [Lattice M] [AddCommGroup M] [Module 𝕜 M] [IsOrderedAddMonoid M] (x y : M) : x ⊓ y = 2⁻¹ • (x + y - |y - x|)

theorem sup_eq_half_smul_add_add_abs_sub' (𝕜 : Type u_1) {M : Type u_3} [DivisionSemiring 𝕜] [NeZero 2] [Lattice M] [AddCommGroup M] [Module 𝕜 M] [IsOrderedAddMonoid M] (x y : M) : x ⊔ y = 2⁻¹ • (x + y + |y - x|)