have abNotTwo
  : ¬ AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
  := abTri.atMostOne
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
ab : ℤ := a - b
abTwo : AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
⊢ False
ℕ : Type
inst✝⁷ : Natural ℕ
ℤ : Type
inst✝⁶ : Core ℤ
inst✝⁵ : Addition ℤ
inst✝⁴ : Multiplication ℤ
inst✝³ : Negation ℤ
inst✝² : Subtraction ℤ
inst✝¹ : Sign ℤ
inst✝ : Order ℤ
a b : ℤ
abTri : AA.ExactlyOneOfThree (a - b ≃ 0) (Positive (a - b)) (Negative (a - b))
x✝ : AA.TwoOfThree (a < b) (a ≃ b) (a > b)
ab : ℤ := a - b
abTwo : AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
abNotTwo : ¬AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
⊢ False