case mpr =>
  intro (_ : lt m n)
  show compare n m = Ordering.gt
  have notTwo : ¬ AA.TwoOfThree (lt n m) (n ≃ m) (lt m n) :=
    (trichotomy (order_inst := order) n m).atMostOne
  simp [compare, Ord.compare, compareOfLessAndEq]
  split
  case isTrue =>
    have : n < m := by assumption
    show False
    have : lt n m := prelude_lt_iff_impl_lt.mp ‹n < m›
    have two : AA.TwoOfThree (lt n m) (n ≃ m) (lt m n) :=
      AA.TwoOfThree.oneAndThree ‹lt n m› ‹lt m n›
    exact absurd two notTwo
  case isFalse =>
    split
    case isTrue =>
      have : n = m := by assumption
      show False
      have : n ≃ m := ‹n = m›
      have two : AA.TwoOfThree (lt n m) (n ≃ m) (lt m n) :=
        AA.TwoOfThree.twoAndThree ‹n ≃ m› ‹lt m n›
      exact absurd two notTwo
    case isFalse =>
      show Ordering.gt = Ordering.gt
      rfl
n m : Nat
⊢ lt m n → compare n m = Ordering.gt
no goals