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

State before:
a b : Fraction
⊢ a ≈ b ↔ a.num * b.denom = b.num * a.denom
Tactic:
rfl
State after:
no goals