feat: add lemmas for Nat/Bits, Nat/Bitwise and Nat/Size

[Command-Master]

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.

---

[Rida-Hamadani]

LGTM!

[Command-Master]

I'm curious what you're using this for - I had it in the back of my mind to remove everything about bit at some point

I'm using it for #12750.

[github-actions[bot]]

PR summary b200eebfe0

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ add_pow_testBit + and_div2 + bit_false_succ + bit_true_succ + bitwise_div2 + div2_testBit + or_div2 + 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>

[YaelDillies]

I know you need these lemmas, but I'm afraid they have no good home anymore. Mind merging master to sort that out?

[Command-Master]

Perhaps they could all go to Mathlib.Data.Nat.Bits? I think I'll try to update #12750 and see what I need

[jcommelin]

This looks like it's pretty close to being mergeable. Could you please merge master and resolve the conflicts?