cases Classical.em (num a' = 0) with
| inl ha'0 =>
  simp [ha0, ha'0, inv_zero]
| inr ha'0 =>
  simp [ha0, ha'0, Setoid_Iff, denom_Neq_zero] at ha
case inl
a a' : Fraction
ha : a ≈ a'
ha0 : a.num = 0
⊢ a⁻¹ ≈ a'⁻¹
no goals