[Merged by Bors] - chore(Data/PNat): drop bit* lemmas

[urkud]

Add OfNat lemmas instead.

---

[github-actions]

PR summary e1c5f4b274

Import changes

No significant changes to the import graph

---

Declarations diff

+ ofNat_inj
+ ofNat_le_ofNat
+ ofNat_lt_ofNat
- bit0_le_bit0
- bit0_le_bit1
- bit1_le_bit0
- bit1_le_bit1

You can run this locally as follows

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

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

[kim-em]

bors merge

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Build failed (retrying...):

• Build

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style