Progress towards showing the connection between ACL2 and HOL ordinals.

In particular, show that the ord_less from ordinalNotation is the same
as < on the “real” ordinals.
A new keybinding for less-than-or-equals in hol-unicode.

C-Q is not great, but the mnemonic is ‘less than or eQuals’.