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