DEFINITION lt_le_S()
TYPE =
       ∀n:nat.∀p:nat.(lt n p)→(le (S n) p)
BODY =
Show proof