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 =
Show proof