α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ abs a = max a 0 + max (-a) 0
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ max a 0 + max (-a) 0 = abs a
symm
no goals
α : Type u_1
inst✝ : LinearOrderedRing α
a✝ b c a : α
⊢ abs a = max a 0 + max (-a) 0
rcases le_total 0 a with (ha | ha) <;> simp [ha]