feat(data/nat/digits): Add lemmas

[Pazzaz]

Add some lemmas about nat.digits and nat.of_digits, including that digits b (of_digits b L) is a prefix of L

---

I found the need for these lemmas while formalizing properties of Kaprekar's routine.

(Note: this is my first PR 🙂)

[bryangingechen]

@Pazzaz gentle ping. Feel free to ask here or on Zulip if you need help with the suggestion above.