Theorem: fformat_prec_lt_0 (HOLFloat/Fixed_theroem.lean)

State before:
fmt : fformat
⊢ 0 < (↑fmt).p
Tactic:
have h := fmt.prop.right.right
State after:
fmt : fformat
h : 0 < (↑fmt).p
⊢ 0 < (↑fmt).p

State before:
fmt : fformat
h : 0 < (↑fmt).p
⊢ 0 < (↑fmt).p
Tactic:
exact h
State after:
no goals