calc
  sgn (a//b)    ≃ _ := Rel.refl
  sgn a         ≃ _ := Rel.symm AA.identR
  sgn a * 1     ≃ _ := AA.substR ‹1 ≃ sgn d›
  sgn a * sgn d ≃ _ := Rel.symm Integer.sgn_compat_mul
  sgn (a * d)   ≃ _ := Integer.sgn_subst ‹a * d ≃ c * b›
  sgn (c * b)   ≃ _ := Integer.sgn_compat_mul
  sgn c * sgn b ≃ _ := AA.substR ‹sgn b ≃ 1›
  sgn c * 1     ≃ _ := AA.identR
  sgn c         ≃ _ := Rel.refl
  sgn (c//d)    ≃ _ := Rel.refl
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝¹ : AP (Positive b)
c d : ℤ
denominator_positive✝ : AP (Positive d)
x✝ : a//b ≃ c//d
this✝³ : a * d ≃ c * b
this✝² : Positive b
this✝¹ : sgn b ≃ 1
this✝ : Positive d
this : 1 ≃ sgn d
⊢ sgn (a//b) ≃ sgn (c//d)
no goals