no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
hab : a ≤ b
hbc : b ≤ c
⊢ b ≤ max (abs a) (abs c)
simp [hbc.trans (le_abs_self c)]
no goals
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
a b c d : α
hab : a ≤ b
hbc : b ≤ c
⊢ -b ≤ max (abs a) (abs c)
simp [((@neg_le_neg_iff α ..).mpr hab).trans (neg_le_abs_self a)]