TileStructure.Forest.le_C7_7_2_2

lemma le_C7_7_2_2 (a4 : 4 ≤ a) :    C7_3_1_2 a * (2 ^ (4 * (a : ℝ) - n + 1)) ^ (2 : ℝ)⁻¹ ≤ C7_7_2_2 a n := by  rw [sub_add_eq_add_sub, sub_eq_add_neg, NNReal.rpow_add two_ne_zero, NNReal.mul_rpow]  conv_lhs => enter [2, 2]; rw [← NNReal.rpow_mul, ← div_eq_mul_inv, neg_div]  conv_rhs => rw [C7_7_2_2, ← NNReal.rpow_natCast]  rw [← mul_assoc]; gcongr  rw [C7_3_1_2, ← NNReal.rpow_mul, ← NNReal.rpow_natCast, ← NNReal.rpow_add two_ne_zero]  gcongr  · exact one_le_two  · simp only [Nat.cast_mul, Nat.cast_add, Nat.cast_ofNat, Nat.cast_pow]    ring_nf    have : (4 : ℝ) ≤ a := mod_cast a4    suffices 1/2 + 2 * (a : ℝ) ≤ a ^ 3 by linarith    calc      _ ≤ 2 * (a : ℝ) + 2 * a := by linarith      _ = 1 * 4 * a := by ring      _ ≤ a * a * a := by gcongr; linarith      _ = _ := by ring