have : a ≃ 0 → a//b ≃ 0 := (eqv_zero_iff_numerator_eqv_zero (p := a//b)).mpr
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
⊢ Integer.Nonzero (a//b).numerator
ℕ : Type
inst✝¹ : Natural ℕ
ℤ : Type
inst✝ : Integer ℤ
a b : ℤ
denominator_positive✝ : AP (Positive b)
x✝ : AP (a//b ≄ 0)
this : a ≃ 0 → a//b ≃ 0
⊢ Integer.Nonzero (a//b).numerator