DEFINITION lt_n_n()
TYPE =
       ∀n:nat.(not (lt n n))
BODY =
Show proof