Change size_t representation in Coq model

Currently it's represented by `nat`, which is the theoretical-mathematics version of a natural number, but it would be better to use `N`, the binary version, since we're never doing mathematical induction on it and it would save silly work converting between the two.