mathlib3

e3d2f74c - feat(data/nat): Add new binary recursors; prove the relationship between `nat.bits` and other pieces of code (#14990)

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.