src/HOL/Orderings.thy

   { fix m assume m: "m < ?x"
     from not_less_Least[OF m] have "\<not> P m" . }
   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
 
 
 subsection \<open>Order on \<^typ>\<open>bool\<close>\<close>