DEFINITION next_plus_lt()
TYPE =
       ∀g:G.∀h:nat.∀n:nat.(lt n (next_plus g (next g n) h))
BODY =
Show proof