Theorem: fformat_valid_imp_prec_lt_0 (HOLFloat/Fixed_theroem.lean)

State before:
fmt : format
⊢ is_valid_fformat fmt → 0 < fmt.p
Tactic:
intro h
State after:
fmt : format
h : is_valid_fformat fmt
⊢ 0 < fmt.p

State before:
fmt : format
h : is_valid_fformat fmt
⊢ 0 < fmt.p
Tactic:
exact h.right.right
State after:
no goals