TileStructure.Forest.le_C7_2_2

lemma le_C7_2_2 (a4 : 4 ≤ a) :    2 * C_Ts a + 2 ^ (7 * a + (𝕔 + 1) * a ^ 3 + 1) * CMB (defaultA a) 2 ≤ C7_2_2 a := by  rw [C_Ts, CMB_defaultA_two_eq]  calc    _ ≤ (2 : ℝ≥0) ^ (a ^ 3 + 1) + 2 ^ (7 * a + (𝕔 + 1) * a ^ 3 + 1) * 2 ^ (a + 2) := by      rw [← pow_succ']; gcongr; rw [← NNReal.rpow_natCast]; push_cast; gcongr <;> norm_num    _ ≤ 2 ^ ((𝕔 + 1) * a ^ 3 + 8 * a + 3) + 2 ^ ((𝕔 + 1) * a ^ 3 + 8 * a + 3) := by      rw [← pow_add]; gcongr 2 ^ ?_ + 2 ^ ?_      · exact one_le_two      · rw [show a ^ 3 + 1 = 1 * a ^ 3 + 1 by ring, add_assoc]; gcongr        · norm_num        · lia      · exact one_le_two      · ring_nf; rfl    _ = 2 ^ ((𝕔 + 1) * a ^ 3 + 8 * a + 4) := by rw [← two_mul, ← pow_succ']    _ ≤ _ := by      rw [C7_2_2, add_assoc, show (𝕔 + 2) * a ^ 3 = (𝕔 + 1) * a ^ 3 + a ^ 3 by ring]      gcongr; · exact one_le_two      calc        _ ≤ 4 * 4 * a := by lia        _ ≤ _ := by rw [pow_three']; gcongr