DEFINITION weight_add_S()
TYPE =
       ∀t:T
         .∀m:nat
           .le
             weight_map (wadd λ:nat.O O) t
             weight_map (wadd λ:nat.O (S m)) t
BODY =
        assume t: T
        assume m: nat
          assume n: nat
             (h1) 
                assume : nat
                   by (le_n .)
                   we proved le O O
nat→(le O O)
             end of h1
             (h2) 
                by (le_O_n .)
                we proved le O m
                by (le_S . . previous)
le O (S m)
             end of h2
             by (wadd_le . . h1 . . h2 .)
             we proved le (wadd λ:nat.O O n) (wadd λ:nat.O (S m) n)
          we proved ∀n:nat.(le (wadd λ:nat.O O n) (wadd λ:nat.O (S m) n))
          by (weight_le . . . previous)
          we proved 
             le
               weight_map (wadd λ:nat.O O) t
               weight_map (wadd λ:nat.O (S m)) t
       we proved 
          ∀t:T
            .∀m:nat
              .le
                weight_map (wadd λ:nat.O O) t
                weight_map (wadd λ:nat.O (S m)) t