Theorem: ipow_le_sum (HOLFloat/Common.lean)

State before:
i : ℕ
r n : ℝ
⊢ 2 ≤ r → 0 ≤ i → ∃ e, n ≤ r ^ e
Tactic:
sorry
State after:
no goals