DEFINITION next_plus_gz()
TYPE =
       ∀n:nat.∀h:nat.(eq nat (next_plus gz n h) (plus h n))
BODY =
Show proof