DEFINITION le_lt_n_Sm()
TYPE =
       ∀n:nat.∀m:nat.(le n m)→(lt n (S m))
BODY =
        assume n: nat
        assume m: nat
        suppose H: le n m
          by (le_n_S . . H)
          we proved le (S n) (S m)
          that is equivalent to lt n (S m)
       we proved ∀n:nat.∀m:nat.(le n m)→(lt n (S m))