src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Sun Nov 28 09:57:48 2021 +0100
+++ b/src/HOL/Wellfounded.thy	Sun Nov 28 19:12:48 2021 +0100
@@ -79,6 +79,9 @@
 lemma (in wellorder) wf: "wf {(x, y). x < y}"
   unfolding wf_def by (blast intro: less_induct)
 
+lemma (in wellorder) wfP_less[simp]: "wfP (<)"
+  by (simp add: wf wfP_def)
+
 
 subsection \<open>Basic Results\<close>