DEFINITION wadd_lt()
TYPE =
       ∀f:nat→nat
         .∀g:nat→nat
           .∀n:nat.(le (f n) (g n))
             →∀v:nat.∀w:nat.(lt v w)→∀n:nat.(le (wadd f v n) (wadd g w n))
BODY =
Show proof