DEFINITION next_plus_gz()
TYPE =
       ∀n:nat.∀h:nat.(eq nat (next_plus gz n h) (plus h n))
BODY =
        assume n: nat
        assume h: nat
          we proceed by induction on h to prove eq nat (next_plus gz n h) (plus h n)
             case O : ⇒
                the thesis becomes eq nat (next_plus gz n O) (plus O n)
                   by (refl_equal . .)
                   we proved eq nat n n
eq nat (next_plus gz n O) (plus O n)
             case S : n0:nat ⇒
                the thesis becomes eq nat (next_plus gz n (S n0)) (plus (S n0) n)
                (H) by induction hypothesis we know eq nat (next_plus gz n n0) (plus n0 n)
                   by (f_equal . . . . . H)
                   we proved eq nat (S (next_plus gz n n0)) (S (plus n0 n))
eq nat (next_plus gz n (S n0)) (plus (S n0) n)
          we proved eq nat (next_plus gz n h) (plus h n)
       we proved ∀n:nat.∀h:nat.(eq nat (next_plus gz n h) (plus h n))