Complex.Gamma.norm_Gamma_le_two_mul_norm_Gamma_add_one

lemma norm_Gamma_le_two_mul_norm_Gamma_add_one {z : ℂ} (hz : z ≠ 0) (hz_lb : (1 / 2 : ℝ) ≤ ‖z‖) :    ‖Gamma z‖ ≤ 2 * ‖Gamma (z + 1)‖ := by  have hfunc := Gamma_add_one z hz  have hnorm_mul : ‖Gamma (z + 1)‖ = ‖z‖ * ‖Gamma z‖ := by    calc      ‖Gamma (z + 1)‖ = ‖z * Gamma z‖ := by simp [hfunc]      _ = ‖z‖ * ‖Gamma z‖ := by simp  have hz_pos : 0 < ‖z‖ := lt_of_lt_of_le (by norm_num) hz_lb  have hz_ne : ‖z‖ ≠ 0 := ne_of_gt hz_pos  have h_inv : 1 / ‖z‖ ≤ (2 : ℝ) := by    have hhalf_pos : (0 : ℝ) < (1 / 2 : ℝ) := by norm_num    simpa using one_div_le_one_div_of_le hhalf_pos hz_lb  have : ‖Gamma z‖ = ‖Gamma (z + 1)‖ / ‖z‖ := by    calc      ‖Gamma z‖ = (‖z‖ * ‖Gamma z‖) / ‖z‖ := by field_simp [hz_ne]      _ = ‖Gamma (z + 1)‖ / ‖z‖ := by simp [hnorm_mul]  rw [this, div_eq_mul_inv]  have :      (‖Gamma (z + 1)‖ : ℝ) * (1 / ‖z‖) ≤ ‖Gamma (z + 1)‖ * 2 :=    mul_le_mul_of_nonneg_left h_inv (norm_nonneg _)  simpa [mul_assoc, mul_left_comm, mul_comm] using this