DEFINITION le_reg_l()
TYPE =
       ∀n:nat.∀m:nat.∀p:nat.(le n m)→(le (plus p n) (plus p m))
BODY =
        assume n: nat
        assume m: nat
        assume p: nat
          we proceed by induction on p to prove (le n m)→(le (plus p n) (plus p m))
             case O : ⇒
                the thesis becomes (le n m)→(le (plus O n) (plus O m))
                   suppose H: le n m
                      consider H
                      we proved le n m
                      that is equivalent to le (plus O n) (plus O m)
(le n m)→(le (plus O n) (plus O m))
             case S : p0:nat ⇒
                the thesis becomes ∀H:(le n m).(le (S (plus p0 n)) (S (plus p0 m)))
                (IHp) by induction hypothesis we know (le n m)→(le (plus p0 n) (plus p0 m))
                   suppose H: le n m
                      by (IHp H)
                      we proved le (plus p0 n) (plus p0 m)
                      by (le_n_S . . previous)
                      we proved le (S (plus p0 n)) (S (plus p0 m))
                      that is equivalent to le (plus (S p0) n) (plus (S p0) m)
∀H:(le n m).(le (S (plus p0 n)) (S (plus p0 m)))
          we proved (le n m)→(le (plus p n) (plus p m))
       we proved ∀n:nat.∀m:nat.∀p:nat.(le n m)→(le (plus p n) (plus p m))