DEFINITION lt_plus_plus()
TYPE =
       ∀n:nat
         .∀m:nat
           .∀p:nat.∀q:nat.(lt 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: lt n m
        suppose H0: lt p q
          by (lt_le_weak . . H0)
          we proved le p q
          by (lt_le_plus_plus . . . . H previous)
          we proved lt (plus n p) (plus m q)
       we proved 
          ∀n:nat
            .∀m:nat
              .∀p:nat.∀q:nat.(lt n m)→(lt p q)→(lt (plus n p) (plus m q))