Theorem: ipow_le_real_two (HOLFloat/Common.lean)

State before:
r z : ℝ
⊢ 0 < z → 2 ≤ r → ∃ e, r ^ e ≤ z
Tactic:
sorry
State after:
no goals