have x_sgn_a {x : ℤ} : x * sgn a ≃ x := calc
  x * sgn a ≃ _ := AA.substR ‹sgn a ≃ 1›
  x * 1     ≃ _ := AA.identR
  x         ≃ _ := Rel.refl
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this : sgn a ≃ 1
⊢ (a//b)⁻¹ ≃ b//a
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this : sgn a ≃ 1
x_sgn_a : ∀ {x : ℤ}, x * sgn a ≃ x
⊢ (a//b)⁻¹ ≃ b//a