Being more precise: I like Spivak not defining addition, multiplication or number. I just want the other steps explicit, like equality transitivity, enough to implement it (for a computer without "mathematical maturity".)

I feel I already know what's needed - but I didn't catch the 0.a=0 omission at first, and there's surely others I'm still missing... Part of the problem is I have too much implicit knowledge.