Theorem: flformat_radix_le_2_real (HOLFloat/Float_theorem.lean)

State before:
fmt : flformat
⊢ 2 ≤ ↑(↑fmt).r
Tactic:
norm_cast
State after:
fmt : flformat
⊢ 2 ≤ (↑fmt).r

State before:
fmt : flformat
⊢ 2 ≤ (↑fmt).r
Tactic:
linarith [Int.lt_add_one_iff.2 fmt.prop.left, fmt.prop.left]
State after:
no goals