have : p ≃ 0 := eqv_zero_iff_numerator_eqv_zero.mpr this
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
p : Fraction ℤ
x✝ : sgn p ≃ 0
this✝ : sgn p.numerator ≃ 0
this : 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
this : p ≃ 0
⊢ p ≃ 0