DEFINITION lt_n_Sn()
TYPE =
       ∀n:nat.(lt n (S n))
BODY =
       assume n: nat
          by (le_n .)
          we proved le (S n) (S n)
          that is equivalent to lt n (S n)
       we proved ∀n:nat.(lt n (S n))