Asymptotics.IsBigO.add_isLittleO_right

lemma Asymptotics.IsBigO.add_isLittleO_right {f g : ℝ → ℝ} (h : g =o[atTop] f) :    f =O[atTop] (f + g) := by  rw [isLittleO_iff] at h ; specialize h (c := 2⁻¹) (by norm_num)  rw [isBigO_iff'']  refine ⟨2⁻¹, by norm_num, ?_⟩  filter_upwards [h] with x h  simp only [norm_eq_abs, Pi.add_apply] at h ⊢  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)