Complex.norm_inv_add_one_sub_inv_le'

lemma norm_inv_add_one_sub_inv_le' {a : ℝ} (ha : 0 < a) (ha1 : a ≤ 1) {z : ℂ}    (hza : a ≤ z.re) (m : ℕ) :    ‖((m : ℂ) + 1)⁻¹ - (z + m)⁻¹‖ ≤ 2 / (a * ((m : ℝ) + 1)) := by  have hm0 : (0 : ℝ) ≤ m := Nat.cast_nonneg m  have hnorm_zm : a * ((m : ℝ) + 1) ≤ ‖z + m‖ := by    have h1 : (z + m).re ≤ ‖z + m‖ := re_le_norm _    rw [add_re, natCast_re] at h1    nlinarith  have hinv : ((m : ℝ) + 1)⁻¹ ≤ (a * ((m : ℝ) + 1))⁻¹ := by    rw [← one_div, ← one_div]    exact one_div_le_one_div_of_le (by positivity) (by nlinarith)  have hinv2 : ‖z + m‖⁻¹ ≤ (a * ((m : ℝ) + 1))⁻¹ := by    rw [← one_div, ← one_div]    exact one_div_le_one_div_of_le (by positivity) hnorm_zm  calc ‖((m : ℂ) + 1)⁻¹ - (z + m)⁻¹‖      ≤ ‖((m : ℂ) + 1)⁻¹‖ + ‖(z + m)⁻¹‖ := norm_sub_le _ _    _ = ((m : ℝ) + 1)⁻¹ + ‖z + m‖⁻¹ := by        rw [norm_inv, norm_inv, norm_natCast_add_one]    _ ≤ 2 / (a * ((m : ℝ) + 1)) := by        rw [div_eq_mul_inv]        linarith