have : lt n m := prelude_lt_iff_impl_lt.mp ‹n < m›
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝ this : n < m
⊢ False
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝ this✝ : n < m
this : lt n m
⊢ False