have : sgn a ≃ 1 := Integer.sgn_positive.mp ‹AP (Positive a)›.ev
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
⊢ (a//b)⁻¹ ≃ b//a
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this : sgn a ≃ 1
⊢ (a//b)⁻¹ ≃ b//a