chore(SetTheory/Ordinal/CantorNormalForm): CNF.exponents and CNF.coeffs

[vihdzp]

We rewrite theorems about the Cantor Normal Form in terms of their lists of exponents and coefficients, instead of awkwardly talking about their first and second entries.

We also put all theorems about the CNF in its own namespace. This keeps us from cluttering the Ordinal namespace, and it also avoids having to prefix everything by CNF_ constantly.

---

• depends on: [Merged by Bors] - chore(SetTheory/Ordinal/CantorNormalForm): cleanup proofs #16998

[github-actions]

PR summary bfe82bc7c1

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ coeffs
+ coeffs_zero
+ exponents
+ exponents_sorted
+ exponents_zero
+ foldr
+ le_log_of_mem_exponents
+ lt_of_mem_coeffs
+ mem_coeffs_iff
+ mem_coeffs_of_mem
+ mem_exponents_iff
+ mem_exponents_of_mem
+ ne_zero
+ of_le_one
+ of_lt
+ one
+ pos_of_mem_coeffs
+ zero_left
+ zero_right
- one_CNF

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>

The doc-module for script/declarations_diff.sh contains some details about this script.

[vihdzp]

I renamed CNF.coefficients to CNF.coeffs for parity with Polynomial.coeffs.

[digama0]

I don't like that this is mixing new theory and unrelated proof cleanup. Please do these things separately.

[vihdzp]

Yeah, looking back at my code cleanup I'm not sure I agree with everything I did. I'll put that in a separate PR and clean up this one afterwards.

[mathlib4-dependent-issues-bot]

This PR/issue depends on:

• [Merged by Bors] - chore(SetTheory/Ordinal/CantorNormalForm): cleanup proofs #16998
  By Dependent Issues (🤖). Happy coding!

[vihdzp]

PR should be ready for review now! Most of the diff is just due to the deprecations, and all the changes here should hopefully be non-controversial.

[YaelDillies]

You have two paragraphs in your PR description. Can you make each paragraph its own PR?