A common small radius

Two positive radii and a positive gap admit a common smaller positive radius whose double square fits in the gap (TauCeti.exists_pos_lt_lt_two_mul_sq_lt).

theorem TauCeti.exists_pos_lt_lt_two_mul_sq_lt {R₀ R₁ d : ℝ} (hR₀ : 0 < R₀) (hR₁ : 0 < R₁) (hd : 0 < d) : ∃ (r : ℝ), (r < R₀ ∧ r < R₁ ∧ 2 * r ^ 2 < d) ∧ 0 < r

Two positive radii and a positive gap admit a common smaller positive radius whose double square fits in the gap.