DEFINITION next_plus()
TYPE =
       G→nat→nat→nat
BODY =
Show proof