ac_rfl
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 * (a'.denom * b'.denom) + b.num * a.denom * (a'.denom * b'.denom) =
    a.num * a'.denom * b.denom * b'.denom + b.num * b'.denom * a.denom * a'.denom
no goals