intro
  (NonzeroWithSign.intro (bm : ℕ) (_ : Positive bm) (_ : b ≃ bs * coe bm))
ℕ : 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)
ℕ : 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
bm : ℕ
pos✝ : Positive bm
eqv✝ : b ≃ bs * coe bm
⊢ NonzeroWithSign (a * b) (as * bs)