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
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝ : ¬n < m
⊢ (if n = m then Ordering.eq else Ordering.gt) = Ordering.gt
no goals