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 : α
ha : 0 ≤ a
hab : a ≤ b
⊢ abs a ≤ abs b
rwa [abs_of_nonneg ha, abs_of_nonneg (ha.trans hab)]