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