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

State before:
a a' : Fraction
hab : a ≈ a'
⊢ -a ≈ -a'
Tactic:
simp [Setoid_Iff] at *
State after:
a a' : Fraction
hab : a.num * a'.denom = a'.num * a.denom
⊢ a.num * a'.denom = a'.num * a.denom

State before:
a a' : Fraction
hab : a.num * a'.denom = a'.num * a.denom
⊢ a.num * a'.denom = a'.num * a.denom
Tactic:
exact hab
State after:
no goals