feat: define Gray code

[Command-Master]

---

Define binary reflected gray code, both as a permutation of Nat and as a permutation of BitVec n, and prove some theorems about them. Additionally, remove @[simp] from Nat.bit_false and Nat.bit_true, as bit0 and bit1 are deprecated, and add some lemmas to Bits, Bitwise and Size.

• [ ] depends on: #12751

[grunweg]

It seems this PR is awaiting action by the PR author: let me label it accordingly.

Looking at the PR description, it seems to me this PR is doing several things at once: usually, you can get your changes merged faster if you split them - especially since these look (to me) like quite different changes.

[leanprover-community-mathlib4-bot]

This PR/issue depends on:

• leanprover-community/mathlib4#12751 By Dependent Issues (🤖). Happy coding!

[github-actions[bot]]

PR summary e2c8b0856b

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.Nat.GrayCode	333

---

Declarations diff

+ add_pow_testBit + and_div2 + bit_false_succ + bit_true_succ + bitwise_div2 + div2_testBit + grayCode + grayCodeInv + grayCodeInv_val + grayCode_prop + grayCode_size + or_div2 + partialGrayCode + partialGrayCode_prop + size_eq_iff_le_and_lt + size_eq_iff_testBit + succ_testBit_zero + xor_div2

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>