refactor(set_theory/ordinal/cantor_normal_form): CNF as an association list

[vihdzp]

We define CNF as an association list, and rename the old unbundled definition to CNF_list. We also restate some theorems using the list.keys and list.lookup API.

Association lists are the most natural structure for the CNF, since the CNF has the following properties:

• it is functional, in that every exponent is assigned at most one coefficient.
• it is ordered, in decreasing order of exponents.
• it is finite in length.

Though some proofs had to be reordered (so that I could use mem_lookup_iff), they've remained minimally changed.

---

• depends on: [Merged by Bors] - feat(data/list/alist): recursion on alist using insert #15434
• depends on: [Merged by Bors] - feat(set_theory/ordinal/arithmetic): miscellaneous arithmetic lemmas #15990
• depends on: [Merged by Bors] - golf(set_theory/ordinal/cantor_normal_form): golf theorems #16009

[ghost]

This PR/issue depends on:

• [Merged by Bors] - feat(data/list/alist): recursion on alist using insert #15434
• [Merged by Bors] - feat(set_theory/ordinal/arithmetic): miscellaneous arithmetic lemmas #15990
• [Merged by Bors] - golf(set_theory/ordinal/cantor_normal_form): golf theorems #16009
  By Dependent Issues (🤖). Happy coding!