feat: add Nat.Digits

[fgdorais]

This PR adds functions for calculating digit representation in any base. Both little-endian and big-endian versions are provided.

[eric-wieser]

I claim that because of this there really is no point having both versions of the function.

[fgdorais]

There is:

• The LE version has an obvious user-friendly recursion pattern but is highly inefficient. (Stack overflow happens before 7000 digits.)
• The BE version is not user-friendly but it is naturally tail-recursive.
• The BE version is used via csimp to make an efficient implementation of the LE version.
• The BE version has an obvious use case that decimal numbers are in BE format.

[fgdorais]

The names used here don't conflict with Mathlib at all. The expected blend-in is to use toDigitsLE (once csimp implemented as the reverse of toDigitsBE) as a more efficient replacement for Mathlib's digitsAux, the whole thing should be invisible to Mathlib users.

[linesthatinterlace]

You might want to consider that #799 ought to be compatible with this. I am sure there's a lemma like this in Mathlib somewhere but I can't find it.

[linesthatinterlace]

(Mathlib has Nat.bits, which modulo finTwoEquiv is the same as this.)

[fgdorais]

Good reminders! This PR is on hiatus until I find time to rethink the overall design.