Redefine well-orders and prove that their order is well-founded

[Columbus240]

I managed to formalise a proof that the order of well-orders is well-founded and would like to add it to the library. I'm still unsure or unhappy with some parts of it and would very much like an opinion on this before merging it or doing further work on it.

I found it an interesting exercise, because most proofs of these facts are done in a set theory with a global membership relation (ZF / ZFC), where canonical representatives of well-orders exist (i.e. the ordinals). But here in Coq we don't have the privilege of this and can only talk "structurally" (in the sense of "structural set theory") about well-ordered sets. Which makes some parts of this branch non-trivial.

Currently this branch does the following:

• Develop the theory of irreflexive, transitive relations in StrictOrders.v. Includes concepts like "an Ensemble is downwards-closed, "the initial-segment of an element", "the supremum of an Ensemble", "upper bounds of Ensembles".
• In WellOrders_new.v do the whole rest.
• I introduced a different definition of well-order (but equivalent using classical logic), which I found on the n-lab. It is better behaved in a constructive setting. An relation is a well-order (in the new definition) if it is well-founded, transitive and whenever two elements have the same initial-segment, they are equal. (initial-segment of x = set of elements strictly smaller than x)
• Adapt WellOrders.v to use the new definition of well-order.
• In Cardinals.v, prove that the order of cardinals lt_cardinal is well-founded. And define and prove existence of initial ordinals.
• A major difference in style to the rest of the topology library is, that I liberally used typeclasses and typeclass inference. Often born out of lazyness.
• There is currently no way to transfer an existing proof of well_order to use the new definition, i.e. to prove WellOrder given total_strict_order and well_founded, although this is possible.
• I used some coqdoc comments to structure WellOrders_new.v. This is done nowhere else in this repo.

Things to do:

• Add a transfer principle from the old definition to the new definition.
• WellOrders_new.v should be merged with WellOrders.v after the editorial changes.