have : Negative (a * b) := negative_iff_sign_neg1.mpr this
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a b : ℤ
inst✝ : Nonzero (a * b)
x✝ : sgn a ≄ sgn b
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
nws_ab : NonzeroWithSign (a * b) (sgn a * sgn b)
this✝ : sgn a * sgn b ≃ -1
this : NonzeroWithSign (a * b) (-1)
⊢ Negative (a * b)
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a b : ℤ
inst✝ : Nonzero (a * b)
x✝ : sgn a ≄ sgn b
left✝ : Sqrt1 (sgn a)
right✝ : Sqrt1 (sgn b)
nws_ab : NonzeroWithSign (a * b) (sgn a * sgn b)
this✝¹ : sgn a * sgn b ≃ -1
this✝ : NonzeroWithSign (a * b) (-1)
this : Negative (a * b)
⊢ Negative (a * b)