feat(order/well_founded): well_founded_lt.has_min, etc.

[vihdzp]

We add some boilerplate code for porting well_founded.has_min to the typeclasses is_well_founded, well_founded_lt, and well_founded_gt.

Besides the usual convenience from using instances, there's two advantages of doing this:

• the lemmas for well_founded_gt no longer have their names backwards (min instead of max)
• we're able to directly state well_founded_lt.min_le and well_founded_gt.le_max in linear orders

---

• depends on: feat(order/rel_classes): housekeeping #18750

Speaking of boilerplate, I'm not even sure we should keep well_founded.min and the like. In a proof, it's always better to use

obtain ⟨s, hs, hlt⟩ := well_founded.has_min s hns

and outside of it, I can't see much use for having a generic minimal element, unless you're already working in a linear order, in which case you can use Inf instead.

Zulip discussion: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/well_founded.2Emin/near/347492784

[ghost]

This PR/issue depends on:

• feat(order/rel_classes): housekeeping #18750
  By Dependent Issues (🤖). Happy coding!