Theorem: float_ipow_le_real (HOLFloat/Float_theorem.lean)

State before:
fmt : flformat
x : ℝ
⊢ ∃ e, x ≤ ↑(↑fmt).r ^ e
Tactic:
apply ipow_le_real
State after:
case a
fmt : flformat
x : ℝ
⊢ 2 ≤ ↑(↑fmt).r

State before:
case a
fmt : flformat
x : ℝ
⊢ 2 ≤ ↑(↑fmt).r
Tactic:
simp [flformat_radix_le_2]
State after:
no goals