Stirling.GammaAux.norm_sub_real_le

lemma norm_sub_real_le {s : ℂ} {a : ℝ} (ha_pos : 0 < a) (ha_lt : a < s.re) : ‖s - a‖ ≤ ‖s‖ := by  have h_sq : (s.re - a) ^ 2 ≤ s.re ^ 2 := by nlinarith  have h1 : Complex.normSq (s - a) ≤ Complex.normSq s := by    simp only [Complex.normSq_apply, Complex.sub_re, Complex.ofReal_re,               Complex.sub_im, Complex.ofReal_im, sub_zero]    linarith [sq_nonneg s.im]  calc    ‖s - a‖ = Real.sqrt (Complex.normSq (s - a)) := by      rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq_eq_abs, abs_of_nonneg (norm_nonneg _)]    _ ≤ Real.sqrt (Complex.normSq s) := Real.sqrt_le_sqrt h1    _ = ‖s‖ := by      rw [Complex.normSq_eq_norm_sq, Real.sqrt_sq_eq_abs, abs_of_nonneg (norm_nonneg _)]