Commit 2022-08-06 05:32 e3d2f74c

feat(data/nat): Add new binary recursors; prove the relationship between nat.bits and other pieces of code (#14990) This is in connection to https://github.com/leanprover-community/mathlib/pull/13208, because I was asked to write to_bits in terms of nat.size and nat.bits, but nat.bits was hard to use (there were no lemmas about it). This PR proves some statements about nat.bits, so that it can finally be used.