DEFINITION lt_reg_r()
TYPE =
       ∀n:nat.∀m:nat.∀p:nat.(lt n m)→(lt (plus n p) (plus m p))
BODY =
        assume n: nat
        assume m: nat
        assume p: nat
        suppose H: lt n m
          (h1) 
             (h1) 
                we proceed by induction on p to prove lt (plus p n) (plus p m)
                   case O : ⇒
                      the thesis becomes lt (plus O n) (plus O m)
                         consider H
                         we proved lt n m
lt (plus O n) (plus O m)
                   case S : n0:nat ⇒
                      the thesis becomes lt (plus (S n0) n) (plus (S n0) m)
                      () by induction hypothesis we know lt (plus n0 n) (plus n0 m)
                         by (lt_reg_l . . . H)
lt (plus (S n0) n) (plus (S n0) m)
lt (plus p n) (plus p m)
             end of h1
             (h2) 
                by (plus_sym . .)
eq nat (plus m p) (plus p m)
             end of h2
             by (eq_ind_r . . . h1 . h2)
lt (plus p n) (plus m p)
          end of h1
          (h2) 
             by (plus_sym . .)
eq nat (plus n p) (plus p n)
          end of h2
          by (eq_ind_r . . . h1 . h2)
          we proved lt (plus n p) (plus m p)
       we proved ∀n:nat.∀m:nat.∀p:nat.(lt n m)→(lt (plus n p) (plus m p))