Theorem: fformat_valid_imp_radix_even (HOLFloat/Fixed_theroem.lean)

State before:
fmt : format
⊢ is_valid_fformat fmt → fmt.r % 2 = 0
Tactic:
intro h
State after:
fmt : format
h : is_valid_fformat fmt
⊢ fmt.r % 2 = 0

State before:
fmt : format
h : is_valid_fformat fmt
⊢ fmt.r % 2 = 0
Tactic:
exact h.right.left
State after:
no goals