src/HOL/Hilbert_Choice.thy

--- a/src/HOL/Hilbert_Choice.thy	Sat Dec 17 15:22:13 2016 +0100
+++ b/src/HOL/Hilbert_Choice.thy	Sat Dec 17 15:22:13 2016 +0100
@@ -657,6 +657,12 @@
   for x :: nat
   unfolding Greatest_def by (rule GreatestM_nat_le) auto
 
+lemma GreatestI_ex: "\<exists>k::nat. P k \<Longrightarrow> \<forall>y. P y \<longrightarrow> y < b \<Longrightarrow> P (GREATEST x. P x)"
+  apply (erule exE)
+  apply (rule GreatestI)
+   apply assumption+
+  done
+
 
 subsection \<open>An aside: bounded accessible part\<close>