have : p.numerator ≃ 0 := Integer.sgn_zero.mpr this
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
this : sgn p.numerator ≃ 0
⊢ p ≃ 0
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
this✝ : sgn p.numerator ≃ 0
this : p.numerator ≃ 0
⊢ p ≃ 0