DEFINITION IsSucc()
TYPE =
       nat→Prop
BODY =
Show proof