DEFINITION le_lt_plus_plus()
TYPE =
       ∀n:nat
         .∀m:nat
           .∀p:nat.∀q:nat.(le n m)→(lt p q)→(lt (plus n p) (plus m q))
BODY =
        assume n: nat
        assume m: nat
        assume p: nat
        assume q: nat
        suppose H: le n m
          we must prove (lt p q)→(lt (plus n p) (plus m q))
          or equivalently (le (S p) q)→(lt (plus n p) (plus m q))
          suppose H0: le (S p) q
             (h1) 
                by (le_plus_plus . . . . H H0)
le (plus n (S p)) (plus m q)
             end of h1
             (h2) 
                by (plus_Snm_nSm . .)
eq nat (plus (S n) p) (plus n (S p))
             end of h2
             by (eq_ind_r . . . h1 . h2)
             we proved le (plus (S n) p) (plus m q)
             that is equivalent to lt (plus n p) (plus m q)
          we proved (le (S p) q)→(lt (plus n p) (plus m q))
          that is equivalent to (lt p q)→(lt (plus n p) (plus m q))
       we proved 
          ∀n:nat
            .∀m:nat
              .∀p:nat.∀q:nat.(le n m)→(lt p q)→(lt (plus n p) (plus m q))