Commit 2023-03-31 22:20 210657c4
View on Github →refactor(order/well_founded): ditch well_founded_iff_has_min'
and well_founded_iff_has_max'
(#15071)
The predicate x ≤ y → y = x
is no more convenient than ¬ x < y
. For this reason, we ditch well_founded.well_founded_iff_has_min'
and well_founded.well_founded_iff_has_max'
in favor of well_founded.well_founded_iff_has_min
(or in some cases, just well_founded.has_min
. We also remove the misplaced lemma well_founded.eq_iff_not_lt_of_le
, and we golf the theorems that used the removed theorems.
The lemma well_founded.well_founded_iff_has_min
has a misleading name when applied on well_founded (>)
, and mildly screws over dot notation and rewriting by virtue of using >
, but a future refactor will fix this.