Commit 2024-07-18 16:46 a14148b4

feat(Order/WellFounded): well-founded of strictly monotone (#14034) This PR is separated off from #12273, which no longer depends on it. We show that an order with a strictly monotone function into an order with WellFoundedLT is itself WellFoundedLT. We also add three dual variants, and provide an instance showing that a Nat-graded order is thus well-founded.