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

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