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

State before:
a b : Fraction
⊢ (a + b).num = a.num * b.denom + b.num * a.denom
Tactic:
rfl
State after:
no goals