exact absurd both not_both
ℕ : Type
inst✝⁶ : Natural ℕ
ℤ : Type
inst✝⁵ : Core ℤ
inst✝⁴ : Addition ℤ
inst✝³ : Multiplication ℤ
inst✝² : Negation ℤ
inst✝¹ : Sign ℤ
a b : ℤ
inst✝ : Nonzero (a * b)
x✝¹ : Negative (a * b)
x✝ : sgn a ≃ sgn b
this : Positive (a * b)
both : Positive (a * b) ∧ Negative (a * b)
not_both : ¬(Positive (a * b) ∧ Negative (a * b))
⊢ False
no goals