152 subsection {* Auxiliary lemmas *}

   152 subsection {* Auxiliary lemmas *}

   153 

   153 

   154 lemma index_minimize:

   154 lemma index_minimize:

   155   assumes "P (i::nat)"

   155   assumes "P (i::nat)"

   156   obtains j where "P j" and "\<forall> k < j. \<not> P k" 

   156   obtains j where "P j" and "\<forall> k < j. \<not> P k" 

   157 proof -

   158 proof -

   158   have "\<exists> j. P j \<and> (\<forall> k < j. \<not> P k)"

   159   have "\<exists> j. P j \<and> (\<forall> k < j. \<not> P k)"

   159   using assms

   160   using assms

   160   proof(induct i rule:less_induct)

   161   proof(induct i rule:less_induct)

   161     case (less t)

   162     case (less t)