R₁_le_D_zpow_div_four

lemma R₁_le_D_zpow_div_four {R₁ : ℝ} : R₁ ≤ D ^ (L302 a R₁ - 1) / 4 := by  rcases le_or_gt R₁ 0 with hR₁ | hR₁; · exact hR₁.trans (by positivity)  rw [le_div_iff₀' zero_lt_four, L302, add_sub_assoc, show (3 - 1 : ℤ) = 2 by norm_num]  have Dg1 := one_lt_realD X  calc    _ = (2 : ℝ) * D ^ Real.logb D (2 * R₁) := by      rw [Real.rpow_logb (realD_pos a) Dg1.ne' (by linarith only [hR₁])]; ring    _ ≤ D * D ^ (⌊Real.logb D (2 * R₁)⌋ + 1) := by      rw [← Real.rpow_intCast]; gcongr      · linarith only [four_le_realD X]      · exact Dg1.le      · push_cast; exact (Int.lt_floor_add_one _).le    _ = _ := by rw [← zpow_one_add₀ (realD_pos a).ne']; congr 1; lia