simp [Setoid_Iff, add_denom, add_num] at *
a a' b b' : Fraction
ha : a ≈ a'
hb : b ≈ b'
⊢ a + b ≈ a' + b'
a a' b b' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
hb : b.num * b'.denom = b'.num * b.denom
⊢ (a.num * b.denom + b.num * a.denom) * (a'.denom * b'.denom) =
    (a'.num * b'.denom + b'.num * a'.denom) * (a.denom * b.denom)