DEFINITION lt_le_S()
TYPE =
       ∀n:nat.∀p:nat.(lt n p)→(le (S n) p)
BODY =
        assume n: nat
        assume p: nat
        suppose H: lt n p
          consider H
          we proved lt n p
          that is equivalent to le (S n) p
       we proved ∀n:nat.∀p:nat.(lt n p)→(le (S n) p)