intro _ _ (_ : a//b ≃ c//d)
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
⊢ ∀ [inst : AP (c//d ≄ 0)] [inst_1 : AP (a//b ≄ 0)], a//b ≃ c//d → (a//b)⁻¹ ≃ (c//d)⁻¹
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
inst✝¹ : AP (c//d ≄ 0)
inst✝ : AP (a//b ≄ 0)
x✝ : a//b ≃ c//d
⊢ (a//b)⁻¹ ≃ (c//d)⁻¹