TileStructure.Forest.le_sq_G2_0_4

lemma le_sq_G2_0_4 (a4 : 4 ≤ a) : C7_7_2_1 a n ^ 2 + C7_7_3 a n * 2 ^ n ≤ G2_0_4 a n ^ 2 := by  simp only [C7_7_2_1, mul_pow, C7_7_3, C7_4_3, C7_4_4, G2_0_4]  have : (2 : ℝ≥0) ^ (- (4 * n : ℝ)) ≤ 2 ^ (- (2 * n : ℝ)) := by gcongr <;> norm_num  grw [this]  simp only [← pow_mul, mul_assoc]  have : (2 : ℝ≥0) ^ (-(2 * n : ℝ)) * 2 ^ n = (2 ^ (-(n / 2 : ℝ))) ^ 2 := by    rw [← NNReal.rpow_natCast, ← NNReal.rpow_add (by norm_num), ← NNReal.rpow_natCast,      ← NNReal.rpow_mul]    ring_nf  rw [this, ← mul_assoc, ← mul_assoc]  simp only [← mul_assoc, ← mul_assoc, ← mul_assoc, ← add_mul, ge_iff_le]  gcongr  rw [← pow_add]  apply (add_le_pow_two_add_cube a4 (by lia) le_rfl).trans ?_  gcongr  · norm_num  have : 𝕔 / 2 ≤ 2 * (𝕔 / 4) + 1 := by lia  grw [this]  ring_nf  lia