TileStructure.Forest.le_C7_5_4

lemma le_C7_5_4 (ha : 4 ≤ a) :    C7_5_9s a * C7_5_10 a + 16 ^ τ * I7_5_4 a ≤ C7_5_4 a := by  have : (16 : ℝ≥0) ^ τ ≤ 2 ^ 1 := by    rw [defaultτ, show (16 : ℝ≥0) = 2 ^ (4 : ℝ) by norm_num, ← NNReal.rpow_mul, ← div_eq_mul_inv,      pow_one]    nth_rw 2 [← NNReal.rpow_one 2]    apply NNReal.rpow_le_rpow_of_exponent_le one_le_two    rw [div_le_one_iff]    norm_cast    lia  grw [this]  simp only [C7_5_9s, C7_5_5, C7_5_10, I7_5_4, C7_5_4, ← pow_add]  apply add_le_pow_two ?_ le_rfl ?_  · ring_nf    suffices 2 + a * 4 ≤ a ^ 3 by lia    linarith [sixteen_times_le_cube ha]  · ring_nf    linarith [sixteen_times_le_cube ha]