DEFINITION lt_n_n()
TYPE =
       ∀n:nat.(not (lt n n))
BODY =
       consider le_Sn_n
       we proved ∀n:nat.(not (le (S n) n))
       that is equivalent to ∀n:nat.(not (lt n n))