have : a ≄ 0 := Integer.nonzero_iff_neqv_zero.mp this
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this : Integer.Nonzero a
⊢ a//b ≄ 0
ℕ : Type
inst✝³ : Natural ℕ
ℤ : Type
inst✝² : Integer ℤ
a b : ℤ
inst✝¹ : AP (Positive a)
inst✝ : AP (Positive b)
this✝ : Integer.Nonzero a
this : a ≄ 0
⊢ a//b ≄ 0