simp [compare, Ord.compare, compareOfLessAndEq]
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
⊢ compare n m = Ordering.gt
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
⊢ (if n < m then Ordering.lt else if n = m then Ordering.eq else Ordering.gt) = Ordering.gt