REPL Unicode input: `\lll` vs. `\verymuchless`

AMS defines `\lll` command for U+022D8 (Very Much Less-Than) character, which is IMHO more "standard" than currently defined `\verymuchless` and more consistent with using `\ggg` for U+022D9 (Very Much Greater-Than).

Therefore, I would suggest using `\lll` instead of (or in addition to) `\verymuchless` completion.

