DEFINITION lt_O_Sn()
TYPE =
       ∀n:nat.(lt O (S n))
BODY =
       assume n: nat
          by (le_O_n .)
          we proved le O n
          by (le_n_S . . previous)
          we proved le (S O) (S n)
          that is equivalent to lt O (S n)
       we proved ∀n:nat.(lt O (S n))