D_zpow_div_two_le_R₂

lemma D_zpow_div_two_le_R₂ {R₂ : ℝ} (hR₂ : 0 < R₂) : D ^ (U302 a R₂) / 2 ≤ R₂ := by  rw [div_le_iff₀' zero_lt_two, U302]  have Dg1 := one_lt_realD X  calc    _ = (D : ℝ)⁻¹ * D ^ (⌈Real.logb D (4 * R₂)⌉ - 1) := by      conv_rhs => rw [mul_comm, ← zpow_sub_one₀ (realD_pos a).ne']      congr 1; lia    _ ≤ 2⁻¹ * (4 * R₂) := by      gcongr; · linarith only [four_le_realD X]      have : 0 < 4 * R₂ := by positivity      nth_rw 2 [← Real.rpow_logb (realD_pos a) Dg1.ne' this]      rw [← Real.rpow_intCast]; gcongr      · exact Dg1.le      · push_cast; rw [sub_le_iff_le_add]; exact (Int.ceil_lt_add_one _).le    _ = _ := by ring