TileStructure.Forest.le_C7_4_3

lemma le_C7_4_3 (ha : 4 ≤ a) : C7_3_1_1 a + CMB (defaultA a) 2 + 1 ≤ C7_4_3 a := by  rw [C7_4_3, C7_3_1_1, CMB_defaultA_two_eq]  calc    _ ≤ (2 : ℝ≥0) ^ ((𝕔 + 6 + 𝕔 / 2 + 𝕔 / 4) * a ^ 3)        + 2 ^ ((a : ℝ) + 3 / 2) + 2 ^ ((a : ℝ) + 3 / 2) := by      gcongr; exact NNReal.one_le_rpow one_le_two (by linarith)    _ = 2 ^ ((𝕔 + 6 + 𝕔 / 2 + 𝕔 / 4) * a ^ 3)  + 2 ^ ((a : ℝ) + 5 / 2) := by      rw [add_assoc, ← two_mul, ← NNReal.rpow_one_add' (by positivity)]; congr 2; ring    _ ≤ 2 ^ ((𝕔 + 6 + 𝕔 / 2 + 𝕔 / 4) * a ^ 3)        + 2 ^ ((𝕔 + 6 + 𝕔 / 2 + 𝕔 / 4 : ℕ) * (a : ℝ) ^ 3) := by      gcongr      · exact one_le_two      · calc          _ ≤ 2 * (a : ℝ) := by            rw [two_mul]; gcongr; exact (show (5 : ℝ) / 2 ≤ 4 by norm_num).trans (mod_cast ha)          _ = 2 * a * 1 * 1 := by ring          _ ≤ (𝕔 + 6 + 𝕔 / 2 + 𝕔 / 4 : ℕ) * a * a * a := by            gcongr            · norm_cast              have := seven_le_c              lia            · norm_cast; lia            · norm_cast; lia          _ = _ := by ring    _ ≤ 2 ^ ((𝕔 + 6 + 𝕔 / 2 + 𝕔 / 4 : ℕ) * (a : ℝ) ^ 3 + 1) := by      rw [← NNReal.rpow_natCast]      simp only [Nat.cast_mul, Nat.cast_add, Nat.cast_ofNat, Nat.cast_pow]      rw [← mul_two, ← NNReal.rpow_add_one' (by positivity)]    _ ≤ _ := by      rw [← NNReal.rpow_natCast]; gcongr      · exact one_le_two      · norm_cast        have : 1 ≤ a ^ 3 := one_le_pow_of_one_le' (by linarith) _        grw [this]        exact le_of_eq (by ring)