DEFINITION le_S_n()
TYPE =
       ∀n:nat.∀m:nat.(le (S n) (S m))→(le n m)
BODY =
        assume n: nat
        assume m: nat
        suppose H: le (S n) (S m)
          we proceed by induction on H to prove le (pred (S n)) (pred (S m))
             case le_n : ⇒
                the thesis becomes le (pred (S n)) (pred (S n))
                   by (le_n .)
                   we proved le n n
le (pred (S n)) (pred (S n))
             case le_S : m0:nat H0:le (S n) m0 ⇒
                the thesis becomes le (pred (S n)) (pred (S m0))
                () by induction hypothesis we know le n (pred m0)
                   by (le_trans_S . . H0)
                   we proved le n m0
le (pred (S n)) (pred (S m0))
          we proved le (pred (S n)) (pred (S m))
          that is equivalent to le n m
       we proved ∀n:nat.∀m:nat.(le (S n) (S m))→(le n m)