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