is_well_founded design

Stream: general

[Violeta Hernández]

So, I've recently added docs#well_founded_lt and docs#well_founded_gt. I'm interested in how to deal with docs#well_founded.min now that we have these.

My proposal is the following:

• Have the API take in a typeclass argument is_well_founded instead of the unbundled well_founded (similar to how we do with e.g. irreflexive or transitive relations).
• Add aliases for both well_founded_lt and well_founded_gt (this way we can write well_founded_gt.max instead of is_well_founded.min (>)).

Note that the well_founded.min API is very small (just four theorems and a fifth min_singleton I want to add), so while this does lead to a bit of code duplication, I believe the convenience we gain out of this is worth it.

[Violeta Hernández]

Also, looking through the current code, we almost always use these theorems on either < or >