Theorem: flformat_radix_lt_1_real (HOLFloat/Float_theorem.lean)

State before:
fmt : flformat
⊢ 1 < ↑(↑fmt).r
Tactic:
norm_cast
State after:
fmt : flformat
⊢ 1 < (↑fmt).r

State before:
fmt : flformat
⊢ 1 < (↑fmt).r
Tactic:
linarith [fmt.prop.left]
State after:
no goals