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