case atMostOne =>
  intro (h : AA.TwoOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m)))
  have twoOfThree : AA.TwoOfThree (n < m) (n ≃ m) (n > m) := match h with
  | AA.TwoOfThree.oneAndTwo (_ : n——m ≃ 0) (_ : Positive (n——m)) =>
    have : n ≃ m := zero_diff_eqv.mp ‹n——m ≃ 0›
    have : n > m := pos_diff_gt.mp ‹Positive (n——m)›
    AA.TwoOfThree.twoAndThree ‹n ≃ m› ‹n > m›
  | AA.TwoOfThree.oneAndThree (_ : n——m ≃ 0) (_ : Negative (n——m)) =>
    have : n < m := neg_diff_lt.mp ‹Negative (n——m)›
    have : n ≃ m := zero_diff_eqv.mp ‹n——m ≃ 0›
    AA.TwoOfThree.oneAndTwo ‹n < m› ‹n ≃ m›
  | AA.TwoOfThree.twoAndThree (_ : Positive (n——m)) (_ : Negative (n——m)) =>
    have : n < m := neg_diff_lt.mp ‹Negative (n——m)›
    have : n > m := pos_diff_gt.mp ‹Positive (n——m)›
    AA.TwoOfThree.oneAndThree ‹n < m› ‹n > m›
  show False
  have notTwoOfThree : ¬ AA.TwoOfThree (n < m) (n ≃ m) (n > m) :=
    natOrderTri.atMostOne
  exact absurd twoOfThree notTwoOfThree
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
⊢ ¬AA.TwoOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
no goals