C5_1_2_optimized_le'

lemma C5_1_2_optimized_le' {a : ℕ} {q : ℝ≥0} (ha : 4 ≤ a) :    C5_1_2_optimized a q ≤ C2_0_4_base a * 2 ^ (a ^ 3) / (q - 1) ^ 4 := by  have : C5_1_2_optimized a q = C2_0_4_base a * (2 ^ (a + 5/2 : ℝ) * 13009) / (q - 1) ^ 4 := by    simp [C5_1_2_optimized, mul_assoc]  rw [this]  gcongr  simp only [← NNReal.coe_le_coe, NNReal.coe_mul, coe_rpow, NNReal.coe_ofNat]  calc  (2 : ℝ) ^ (a + 5 / 2 : ℝ) * 13009  _ ≤ 2 ^ (a + 3 : ℝ) * 2 ^ 14 := by gcongr <;> norm_num  _ = 2 ^ (a + 17) := by    have : (a + 3 : ℝ) = (a + 3 : ℕ) := by norm_cast    rw [this, Real.rpow_natCast, ← pow_add]  _ ≤ 2 ^ (a ^ 3) := by    apply pow_le_pow_right₀ one_le_two    have : (4 : ℤ) ≤ a := mod_cast ha    zify    calc (a : ℤ) + 17    _ ≤ a + 4 * (4 * 4 - 1) := by gcongr; norm_num    _ ≤ a + a * (a * a - 1) := by gcongr    _ = a ^ 3 := by ring