DEFINITION wadd_le()
TYPE =
       ∀f:nat→nat
         .∀g:nat→nat
           .∀n:nat.(le (f n) (g n))
             →∀v:nat.∀w:nat.(le v w)→∀n:nat.(le (wadd f v n) (wadd g w n))
BODY =
        assume f: nat→nat
        assume g: nat→nat
        suppose H: ∀n:nat.(le (f n) (g n))
        assume v: nat
        assume w: nat
        suppose H0: le v w
        assume n: nat
          we proceed by induction on n to prove le (wadd f v n) (wadd g w n)
             case O : ⇒
                the thesis becomes le (wadd f v O) (wadd g w O)
                   consider H0
                   we proved le v w
le (wadd f v O) (wadd g w O)
             case S : n0:nat ⇒
                the thesis becomes le (wadd f v (S n0)) (wadd g w (S n0))
                () by induction hypothesis we know le (wadd f v n0) (wadd g w n0)
                   by (H .)
                   we proved le (f n0) (g n0)
le (wadd f v (S n0)) (wadd g w (S n0))
          we proved le (wadd f v n) (wadd g w n)
       we proved 
          ∀f:nat→nat
            .∀g:nat→nat
              .∀n:nat.(le (f n) (g n))
                →∀v:nat.∀w:nat.(le v w)→∀n:nat.(le (wadd f v n) (wadd g w n))