Commit 2025-01-22 18:42 2cb1216e
View on Github →chore(Order/WellFoundedSet): flip isWF_iff_isPWO (#20937)
Iff lemmas are generally of the form complicated thing ↔ simpler thing, and being a PWO is more complicated than being a well-founded set (in the sense that PWOs are well-founded sets with extra conditions).