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 =
        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: lt 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 lt v w
                   that is equivalent to le (S v) w
                   by (le_S . . previous)
                   we proved le (S v) (S w)
                   by (le_S_n . . previous)
                   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.(lt v w)→∀n:nat.(le (wadd f v n) (wadd g w n))