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
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
no goals