Complex.Hadamard.norm_div_le_half_of_norm_le_of_two_mul_lt

lemma norm_div_le_half_of_norm_le_of_two_mul_lt {z a : ℂ} {R : ℝ}    (hR : 0 < R) (hz : ‖z‖ ≤ R) (ha : (2 * R : ℝ) < ‖a‖) :    ‖z / a‖ ≤ (1 / 2 : ℝ) := by  have h2R_pos : 0 < (2 * R : ℝ) := by nlinarith [hR]  have hinv : ‖a‖⁻¹ < (2 * R)⁻¹ := by    simpa [one_div] using one_div_lt_one_div_of_lt h2R_pos ha  have hmul_le : ‖z‖ * ‖a‖⁻¹ ≤ R * ‖a‖⁻¹ :=    mul_le_mul_of_nonneg_right hz (inv_nonneg.2 (norm_nonneg a))  have hmul_lt : R * ‖a‖⁻¹ < R * (2 * R)⁻¹ :=    mul_lt_mul_of_pos_left hinv hR  have hRhalf : R * (2 * R)⁻¹ = (1 / 2 : ℝ) := by    have hRne : (R : ℝ) ≠ 0 := hR.ne'    rw [show R * (2 * R)⁻¹ = R / (2 * R) by simp [div_eq_mul_inv]]    field_simp [hRne]  have hnorm : ‖z / a‖ = ‖z‖ * ‖a‖⁻¹ := by    simp [div_eq_mul_inv]  exact le_of_lt <| by    calc      ‖z / a‖ = ‖z‖ * ‖a‖⁻¹ := hnorm      _ ≤ R * ‖a‖⁻¹ := hmul_le      _ < R * (2 * R)⁻¹ := hmul_lt      _ = (1 / 2 : ℝ) := hRhalf