Theorem: LoVe.Fraction.inv_num (LoVe/Lectures/LoVe14_RationalAndRealNumbers_Demo.lean)

State before:
a : Fraction
ha : a.num ≠ 0
⊢ a⁻¹.num = a.denom
Tactic:
rw [inv_def a ha]
State after:
no goals