Complex.norm_weierstrassFactor_div_sub_one_le_pow_div

lemma norm_weierstrassFactor_div_sub_one_le_pow_div (m : ℕ) {a z : ℂ}    (hza : ‖z‖ ≤ ‖a‖ / 2) :    ‖weierstrassFactor m (z / a) - 1‖ ≤ 4 * ‖z‖ ^ (m + 1) / ‖a‖ ^ (m + 1) := by  by_cases ha : a = 0  · have hz : z = 0 := by      apply norm_eq_zero.mp      rw [ha] at hza      simpa using hza    subst z    simp [ha]  · have ha' : 0 < ‖a‖ := norm_pos_iff.mpr ha    have hza' : ‖z / a‖ ≤ 1 / 2 := by      rw [Complex.norm_div, div_le_iff₀ ha']      simpa [div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc] using hza    have hbase := weierstrassFactor_sub_one_pow_bound (m := m) (z := z / a) hza'    calc      ‖weierstrassFactor m (z / a) - 1‖ ≤ ‖z‖ ^ (m + 1) / ‖a‖ ^ (m + 1) * 4 := by        simpa [Complex.norm_div, div_pow, mul_comm, mul_left_comm, mul_assoc] using hbase      _ = 4 * ‖z‖ ^ (m + 1) / ‖a‖ ^ (m + 1) := by ring