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.

---