case atMostOne =>
  intro (_ : AA.TwoOfThree (a < b) (a ≃ b) (a > b))
  show False
  let ab := a - b
  have abTwo : AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab) :=
    match ‹AA.TwoOfThree (a < b) (a ≃ b) (a > b)› with
    | AA.TwoOfThree.oneAndTwo (_ : a < b) (_ : a ≃ b) =>
      have : Negative ab := lt_iff_neg_diff.mp ‹a < b›
      have : ab ≃ 0 := zero_diff_iff_eqv.mpr ‹a ≃ b›
      AA.TwoOfThree.oneAndThree ‹ab ≃ 0› ‹Negative ab›
    | AA.TwoOfThree.oneAndThree (_ : a < b) (_ : a > b) =>
      have : Negative ab := lt_iff_neg_diff.mp ‹a < b›
      have : Positive ab := gt_iff_pos_diff.mp ‹a > b›
      AA.TwoOfThree.twoAndThree ‹Positive ab› ‹Negative ab›
    | AA.TwoOfThree.twoAndThree (_ : a ≃ b) (_ : a > b) =>
      have : ab ≃ 0 := zero_diff_iff_eqv.mpr ‹a ≃ b›
      have : Positive ab := gt_iff_pos_diff.mp ‹a > b›
      AA.TwoOfThree.oneAndTwo ‹ab ≃ 0› ‹Positive ab›
  have abNotTwo
    : ¬ AA.TwoOfThree (ab ≃ 0) (Positive ab) (Negative ab)
    := abTri.atMostOne
  exact absurd abTwo abNotTwo
ℕ : 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))
⊢ ¬AA.TwoOfThree (a < b) (a ≃ b) (a > b)
no goals