Theorem: fformat_valid_imp_radix_lt_one (HOLFloat/Fixed_theroem.lean)

State before:
fmt : format
⊢ is_valid_fformat fmt → 1 < fmt.r
Tactic:
intro h
State after:
fmt : format
h : is_valid_fformat fmt
⊢ 1 < fmt.r

State before:
fmt : format
h : is_valid_fformat fmt
⊢ 1 < fmt.r
Tactic:
exact h.left
State after:
no goals