4.2.2 "That means considering two cases separately: the incoming value is either zero or non-zero: that is, either nat.zero, or nat.succ n’ for some “one-smaller” value, n’." Does this mean that it will be defined inductively or am I just being a silly goose? #33