Fix comment about no-maximal-ordinal
Delete note about ordinal arithmetic below ω being the same as on :num.
Minor edits in division section.
Slight cuts in CNF section.
Polish sentence on ordinal notations à la Coq and ACL2.
Some polishing in ACL2 validation section.
Shorten “abuse of notation” parenthetical remark.
Some polishing in construction of ordinals section.