DEFINITION lt_le_plus_plus()
TYPE =
       ∀n:nat
         .∀m:nat
           .∀p:nat.∀q:nat.(lt n m)→(le p q)→(lt (plus n p) (plus m q))
BODY =
        assume n: nat
        assume m: nat
        assume p: nat
        assume q: nat
          we must prove (lt n m)→(le p q)→(lt (plus n p) (plus m q))
          or equivalently (le (S n) m)→(le p q)→(lt (plus n p) (plus m q))
           suppose H: le (S n) m
           suppose H0: le p q
             by (le_plus_plus . . . . H H0)
             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 n) m)→(le p q)→(lt (plus n p) (plus m q))
          that is equivalent to (lt n m)→(le p q)→(lt (plus n p) (plus m q))
       we proved 
          ∀n:nat
            .∀m:nat
              .∀p:nat.∀q:nat.(lt n m)→(le p q)→(lt (plus n p) (plus m q))