calc _ = |f x| - 2⁻¹ * |f x| := by ring
     _ ≤ |f x| - |g x| := by linarith
     _ ≤ |(|f x| - |g x|)| := le_abs_self _
     _ ≤ _ := by rw [← sub_neg_eq_add, ← abs_neg (g x)] ; exact abs_abs_sub_abs_le (f x) (-g x)
case h
n : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f g : ℝ → ℝ
h✝ : ∀ᶠ (x : ℝ) in atTop, ‖g x‖ ≤ 2⁻¹ * ‖f x‖
x : ℝ
h : |g x| ≤ 2⁻¹ * |f x|
⊢ 2⁻¹ * |f x| ≤ |f x + g x|
no goals