[hyperthesis]

Thanks, I'll take a look at those late chapters.

The algebra is my main interest, that happens to be in a calculus text.

0a = 0 is proven later in ch 1, it's just the ordering.

By "something I could code", I mean implementimg these properties (more like writing a proof assistant).

[hyperthesis]

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.