have : NonzeroWithSign ab (s * s) :=
  mul_preserves_nonzeroWithSign nwsa nwsb
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝¹ : NonzeroWithSign a s
this✝ : NonzeroWithSign b s
this : s * s ≃ 1
⊢ Positive ab
ℕ : Type
inst✝⁵ : Natural ℕ
ℤ : Type
inst✝⁴ : Core ℤ
inst✝³ : Addition ℤ
inst✝² : Multiplication ℤ
inst✝¹ : Negation ℤ
inst✝ : Sign ℤ
a b : ℤ
ab : ℤ := a * b
x✝ : SameSign a b
s : ℤ
sqrt1✝ : Sqrt1 s
nwsa : NonzeroWithSign a s
nwsb : NonzeroWithSign b s
this✝² : NonzeroWithSign a s
this✝¹ : NonzeroWithSign b s
this✝ : s * s ≃ 1
this : NonzeroWithSign ab (s * s)
⊢ Positive ab