intro
  (NonzeroWithSign.intro (am : ℕ) (_ : Positive am) (_ : a ≃ as * coe am))
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
⊢ NonzeroWithSign a as → NonzeroWithSign b bs → NonzeroWithSign (a * b) (as * bs)
ℕ : Type
inst✝⁴ : Natural ℕ
ℤ : Type
inst✝³ : Core ℤ
inst✝² : Addition ℤ
inst✝¹ : Multiplication ℤ
inst✝ : Negation ℤ
a b as bs : ℤ
a_sqrt1 : Sqrt1 as
b_sqrt1 : Sqrt1 bs
am : ℕ
pos✝ : Positive am
eqv✝ : a ≃ as * coe am
⊢ NonzeroWithSign b bs → NonzeroWithSign (a * b) (as * bs)