Theorem: fformat_radix_lt_1 (HOLFloat/Fixed_theroem.lean)

State before:
⊢ ∀ (fmt : fformat), 1 < (↑fmt).r
Tactic:
intro h
State after:
h : fformat
⊢ 1 < (↑h).r

State before:
h : fformat
⊢ 1 < (↑h).r
Tactic:
exact h.prop.left
State after:
no goals