simp [Setoid_Iff, ha0, ha'0] at *
case inr.inr
a a' : Fraction
ha : a ≈ a'
ha0 : ¬a.num = 0
ha'0 : ¬a'.num = 0
⊢ a⁻¹ ≈ a'⁻¹
case inr.inr
a a' : Fraction
ha : a.num * a'.denom = a'.num * a.denom
ha0 ha'0 : True
⊢ a.denom * a'.num = a'.denom * a.num