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
n m : Nat
x✝ : lt m n
notTwo : ¬AA.TwoOfThree (lt n m) (n ≃ m) (lt m n)
h✝ : n < m
⊢ False
no goals