Complex.norm_inv_add_one_sub_inv_le

lemma norm_inv_add_one_sub_inv_le {a R : ℝ} (ha : 0 < a) (ha1 : a ≤ 1) {z : ℂ}    (hza : a ≤ z.re) (hzR : ‖z‖ ≤ R) (m : ℕ) :    ‖((m : ℂ) + 1)⁻¹ - (z + m)⁻¹‖ ≤ (R + 1) / (a * ((m : ℝ) + 1) ^ 2) := by  have hm0 : (0 : ℝ) ≤ m := Nat.cast_nonneg m  have hR0 : (0 : ℝ) ≤ R := le_trans (norm_nonneg z) hzR  have hrepos : 0 < (z + m).re := by    rw [add_re, natCast_re]    linarith  have hzm : z + m ≠ 0 := fun h => by simp [h] at hrepos  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 hz1 : ‖z - 1‖ ≤ R + 1 := le_trans (norm_sub_le z 1) (by rw [norm_one]; linarith)  rw [inv_add_one_sub_inv_eq hzm, norm_mul, norm_inv, norm_mul, norm_natCast_add_one,    ← div_eq_mul_inv]  calc ‖z - 1‖ / (((m : ℝ) + 1) * ‖z + m‖)      ≤ (R + 1) / (((m : ℝ) + 1) * (a * ((m : ℝ) + 1))) := by        gcongr    _ = (R + 1) / (a * ((m : ℝ) + 1) ^ 2) := by ring_nf