Commit 2021-11-03 09:54 28111cf3

feat(Init/Data/Nat/Lemmas); nat to string length lemmas (#77) Add lemmas about the length of strings produced by core's Nat.toDigitsCore, and Nat.repr. I needed repr_length and to_digits_core_length for making guarantees about padded string lengths in ISO 8601 times and figured they might be useful for other users doing software stuff (if the maintainers feel differently just reject the PR). As indicated by the doc comment, to_digits_core works for bases greater than one, so it should also work for binary and hex. I found the new digit printing function to be a little bit difficult to work with so the proofs are kind of long.