There is very important subtle difference between you alt_subn and Nat.sub: the line N0 => N0 is N0 => a which gives the same result but makes the termination checking work. I though this was explained in the book but I don't remember precisely.