α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ max a b - min a b = abs (a - b)
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ max a b - min a b = abs (b - a)
rw [abs_sub_comm]
no goals
α : Type u_1
inst✝³ : AddGroup α
inst✝² : LinearOrder α
inst✝¹ : CovariantClass α α (fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a✝ b✝ c : α
inst✝ : CovariantClass α α (swap fun x x_1 => x + x_1) fun x x_1 => x ≤ x_1
a b : α
⊢ max a b - min a b = abs (a - b)
exact max_sub_min_eq_abs' _ _