src/HOL/Orderings.thy

--- a/src/HOL/Orderings.thy	Fri Jun 06 16:18:44 2025 +0100
+++ b/src/HOL/Orderings.thy	Fri Jun 06 18:36:29 2025 +0100
@@ -1392,6 +1392,10 @@
   with LeastI_ex[OF H] show ?rhs by blast
 qed
 
+lemma exists_least_iff': 
+  shows "(\<exists>n. P n) \<longleftrightarrow> P (Least P) \<and> (\<forall>m < (Least P). \<not> P m)"
+  using LeastI_ex not_less_Least by auto
+
 end