have : a * b ≃ (as * bs) * coe (am * bm) := calc
  a * b                         ≃ _ := AA.substL ‹a ≃ as * coe am›
  (as * coe am) * b             ≃ _ := AA.substR ‹b ≃ bs * coe bm›
  (as * coe am) * (bs * coe bm) ≃ _ := AA.expr_xxfxxff_lr_swap_rl
  (as * bs) * (coe am * coe bm) ≃ _ := AA.substR (Rel.symm AA.compat₂)
  (as * bs) * coe (am * bm)     ≃ _ := Rel.refl
ℕ : 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
this : Positive (am * bm)
⊢ 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
this✝ : Positive (am * bm)
this : a * b ≃ as * bs * coe (am * bm)
⊢ NonzeroWithSign (a * b) (as * bs)