feat(order/well_founded): typeclasses for well-founded < and > (#15399)

Well-founded typeclasses

We introduce a new unbundled typeclass is_well_founded for a general well-founded relation, and reducible defs well_founded_lt and well_founded_gt for well-founded < and > specifically, to be used as mixins. For now, all we do is specialize only the most basic API on well-founded relations to these new typeclasses. This is just an initial development. If this is merged, a subsequent PR will redefine is_well_order in terms of is_well_founded (and remove the redundant irrefl field). Further PRs will focus on providing all the possible instances for this new typeclass, and actually using it throughout mathlib. Moved from #15023.

Why do we want this?

Here's the part where I justify why this is a good thing we want in mathlib.

Well-ordered <

There is a need to talk about well-ordered < relations, as a quick search for is_well_order α (<) or is_well_order ι (<) reveals. The most obvious way to spell this condition out, namely [has_lt α] [is_well_order α (<)] is actually the most inconvenient, since none of the results for linear orders are available. You actually need to write [linear_order α] [is_well_order α (<)] instead. With this new typeclass, the obvious spelling is now the good one: [linear_order α] [well_founded_lt α]

Redundant typeclasses

We actually already at least four typeclasses for the well-foundedness of a concrete relation: category.noetherian_object, category.artinian_object, topological_space.noetherian_space, and wf_dvd_monoid. One currently needs to specialize the characterizing properties of a well-founded relation to these separate typeclasses in order to use them. Redefining these typeclasses in terms of these new ones, and making them reducible defs, would alleviate this problem.

Typeclass inference

Well-founded relations are actually a nice candidate for typeclass inference, since there's many common constructions that automatically preserve well-foundedness. These include taking inverse images (including measure and order.preimage), maps through relation embeddings (including subtypes), lexicographic sums or products, and adding a top or bottom element. Many of these are currently provided as instances, but only for well-orders.

Misleading theorem names

Perhaps the most useful result on well-founded relations is that every nonempty set has a minimum - when you view the relation as <, that is. This leads to misleading theorem names when you're using them on a well-founded > relation. With this refactor, we could simply specialize well_founded.min into well_founded_gt.max and end up with clearer theorem statements. On a related note, given a linear order and a well-founded < relation, we can rephrase well_founded.not_lt_min into the much more convenient well_founded_lt.min_le.