have : 1 ≃ sgn d := Rel.symm (Integer.sgn_positive.mp this)
ℕ : 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
⊢ sgn (a//b) ≃ sgn (c//d)
ℕ : 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)