match natOrderTri.atLeastOne with
| AA.OneOfThree.first (_ : n < m) =>
  have : Negative (n——m) := neg_diff_lt.mpr ‹n < m›
  exact AA.OneOfThree.third ‹Negative (n——m)›
| AA.OneOfThree.second (_ : n ≃ m) =>
  have : n——m ≃ 0 := zero_diff_eqv.mpr ‹n ≃ m›
  exact AA.OneOfThree.first ‹n——m ≃ 0›
| AA.OneOfThree.third (_ : n > m) =>
  have : Positive (n——m) := pos_diff_gt.mpr ‹n > m›
  exact AA.OneOfThree.second ‹Positive (n——m)›
ℕ : Type
inst✝ : Natural ℕ
n m : ℕ
natOrderTri : AA.ExactlyOneOfThree (n < m) (n ≃ m) (n > m)
⊢ AA.OneOfThree (n——m ≃ 0) (Positive (n——m)) (Negative (n——m))
no goals