DEFINITION next_plus_lt()
TYPE =
       ∀g:G.∀h:nat.∀n:nat.(lt n (next_plus g (next g n) h))
BODY =
        assume g: G
        assume h: nat
          we proceed by induction on h to prove ∀n0:nat.(lt n0 (next_plus g (next g n0) h))
             case O : ⇒
                the thesis becomes ∀n:nat.(lt n (next_plus g (next g n) O))
                   assume n: nat
                      by (next_lt . .)
                      we proved lt n (next g n)
                      that is equivalent to lt n (next_plus g (next g n) O)
∀n:nat.(lt n (next_plus g (next g n) O))
             case S : n:nat ⇒
                the thesis becomes ∀n0:nat.(lt n0 (next g (next_plus g (next g n0) n)))
                (H) by induction hypothesis we know ∀n0:nat.(lt n0 (next_plus g (next g n0) n))
                   assume n0: nat
                      by (next_plus_next . . .)
                      we proved 
                         eq
                           nat
                           next_plus g (next g (next g n0)) n
                           next g (next_plus g (next g n0) n)
                      we proceed by induction on the previous result to prove lt n0 (next g (next_plus g (next g n0) n))
                         case refl_equal : ⇒
                            the thesis becomes lt n0 (next_plus g (next g (next g n0)) n)
                               (h1) 
                                  by (next_lt . .)
lt n0 (next g n0)
                               end of h1
                               (h2) 
                                  by (H .)
lt (next g n0) (next_plus g (next g (next g n0)) n)
                               end of h2
                               by (lt_trans . . . h1 h2)
lt n0 (next_plus g (next g (next g n0)) n)
                      we proved lt n0 (next g (next_plus g (next g n0) n))
                      that is equivalent to lt n0 (next_plus g (next g n0) (S n))
∀n0:nat.(lt n0 (next g (next_plus g (next g n0) n)))
          we proved ∀n0:nat.(lt n0 (next_plus g (next g n0) h))
       we proved ∀g:G.∀h:nat.∀n0:nat.(lt n0 (next_plus g (next g n0) h))