intro (Nonzero.intro bs (_ : Sqrt1 bs) nwsb)
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝ : Sqrt1 as
nwsa : NonzeroWithSign a as
⊢ Nonzero b → Nonzero (a * b)
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as : ℤ
sqrt1✝¹ : Sqrt1 as
nwsa : NonzeroWithSign a as
bs : ℤ
sqrt1✝ : Sqrt1 bs
nwsb : NonzeroWithSign b bs
⊢ Nonzero (a * b)