DEFINITION le_plus_plus()
TYPE =
       ∀n:nat
         .∀m:nat
           .∀p:nat.∀q:nat.(le n m)→(le p q)→(le (plus n p) (plus m q))
BODY =
        assume n: nat
        assume m: nat
        assume p: nat
        assume q: nat
        suppose H: le n m
        suppose H0: le p q
          we proceed by induction on H to prove le (plus n p) (plus m q)
             case le_n : ⇒
                the thesis becomes le (plus n p) (plus n q)
                   by (le_reg_l . . . H0)
le (plus n p) (plus n q)
             case le_S : m0:nat :le n m0 ⇒
                the thesis becomes le (plus n p) (plus (S m0) q)
                (H2) by induction hypothesis we know le (plus n p) (plus m0 q)
                   by (le_S . . H2)
                   we proved le (plus n p) (S (plus m0 q))
le (plus n p) (plus (S m0) q)
          we proved le (plus n p) (plus m q)
       we proved 
          ∀n:nat
            .∀m:nat
              .∀p:nat.∀q:nat.(le n m)→(le p q)→(le (plus n p) (plus m q))