max and min in terms of the absolute value

max a b = 2⁻¹ * (a + b + |a - b|) and min a b = 2⁻¹ * (a + b - |a - b|).

theorem max_eq_add_add_abs_sub {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a b : α) : max a b = 2⁻¹ * (a + b + |a - b|)

theorem min_eq_add_sub_abs_sub {α : Type u_1} [Field α] [LinearOrder α] [IsStrictOrderedRing α] (a b : α) : min a b = 2⁻¹ * (a + b - |a - b|)