C5_1_3_optimized_le_C5_1_3

lemma C5_1_3_optimized_le_C5_1_3 : C5_1_3_optimized a nnq ≤ C5_1_3 a nnq := by  simp only [C5_1_3_optimized, C5_1_3, C2_0_3]  calc    _ ≤ 2 ^ ((𝕔 + 5 + 𝕔 / 8) * a ^ 3) / (nnq - 1) * 2 ^ (3 * a ^ 3) / (nnq - 1) ^ 4 := by      have := four_le_a X      gcongr; · exact one_le_two      calc        _ ≤ 3 * 4 * 4 * a := by lia        _ ≤ 3 * a * a * a := by gcongr        _ = _ := by ring    _ = 2 ^ ((𝕔 + 5 + 𝕔 / 8) * a ^ 3 + 3 * a ^ 3) / (nnq - 1) ^ (4 + 1) := by      rw [pow_add, pow_add, div_mul_eq_div_div]      simp only [div_eq_inv_mul, pow_one]      ring    _ = _ := by congr; ring