feat: SuccOrder and recursion principle on well-ordered type

[alreadydone]

Order/SuccPred/Basic.lean: add SuccOrder.ofLinearWellFoundedLT, which puts a SuccOrder on an arbitrary well-ordered type. Also add the dual, PredOrder version. Add missing pred lemmas corresponding to existing succ lemmas.

Order/SuccPred/Limit.lean: add SuccOrder.limitRecOn generalizing Ordinal.limitRecOn to allow definition by transfinite recursion on an arbitrary well-ordered type. (It turns out a partial well-founded order is enough.)

SetTheory/Ordinal/Arithmetic.lean: refactor Ordinal.limitRecOn to use SuccOrder.limitRecOn.

SetTheory/Cardinal/Ordinal.lean: add a lemma saying that the initial ordinal of an infinite cardinal is a NoMaxOrder.

SetTheory/Ordinal/Basic.lean: add mk_Iio_ord_out_α, a restatement of card_typein_out_lt.

---

[alreadydone]

cc @digama0, the author of ordinal.limit_rec_on.

[jcommelin]

bors d+

[mathlib-bors[bot]]

:v: alreadydone can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[alreadydone]

Thanks for the review and delegation!

[leanprover-community-mathlib4-bot]

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

[mathlib-bors[bot]]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style