have : n = m := by assumption
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝¹ : ¬n < m
h✝ : n = m
⊢ False
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝¹ : ¬n < m
h✝ this : n = m
⊢ False