revert p₂
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p₂ : Fraction ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ a//b ≃ p₂ → sgn (a//b) ≃ sgn p₂
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
⊢ ∀ {p₂ : Fraction ℤ}, a//b ≃ p₂ → sgn (a//b) ≃ sgn p₂