[Merged by Bors] - refactor(set_theory/ordinal/*): ordinal.succ → order.succ

[vihdzp]

We inline the definition of ordinal.succ in the succ_order instance. This allows us to comfortably use all of the theorems about order.succ to our advantage.

---

(edit by @eric-wieser: tagged as easy since I've reviewed the diff, all we need is a "yes, generalization is worth more than dot notation" opinion by a user of ordinal)

[vihdzp]

I'm reworking this to completely replace ordinal.succ by order.succ.

[eric-wieser]

You need to update the module docstrnig to reference order.succ.

[eric-wieser]

I won't make the call on whether we actually want to do this (someone who's worked with ordinals should answer that), but assuming we do then this PR looks great.

There's one place where you've forgotten to update a module docstring; can you go through the docstrings looking for succ` and add order. prefixes where appropriate?

[vihdzp]

I think this is a good idea, since it means we can reuse the results from order.succ without having to rewrite back and forth. I don't believe ordinals make this a better or worse idea than it would be elsewhere.

[vihdzp]

I should mention - I had to add a lot of explicit order. annotations, but they should go away once #14273 is merged, when there's no longer ambiguity between cardinal and ordinal lemmas.

[fpvandoorn]

bors merge.

This looks great!

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests