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