calc
  (a//b)⁻¹                 ≃ _ := eqv_refl
  (b * sgn a)//(a * sgn a) ≃ _ := substN x_sgn_a
  b//(a * sgn a)           ≃ _ := substD x_sgn_a
  b//a                     ≃ _ := eqv_refl
ℕ : 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
no goals