src/HOLCF/CompactBasis.thy

   assumes take_take: "take n (take n a) = take n a"
   assumes take_mono: "a \<preceq> b \<Longrightarrow> take n a \<preceq> take n b"
   assumes take_chain: "take n a \<preceq> take (Suc n) a"
   assumes finite_range_take: "finite (range (take n))"
   assumes take_covers: "\<exists>n. take n a = a"
+begin
+
+lemma take_chain_less: "m < n \<Longrightarrow> take m a \<preceq> take n a"
+by (erule less_Suc_induct, rule take_chain, erule (1) r_trans)
+
+lemma take_chain_le: "m \<le> n \<Longrightarrow> take m a \<preceq> take n a"
+by (cases "m = n", simp add: r_refl, simp add: take_chain_less)
+
+end
 
 locale ideal_completion = basis_take +
   fixes principal :: "'a::type \<Rightarrow> 'b::cpo"
   fixes rep :: "'b::cpo \<Rightarrow> 'a::type set"
   assumes ideal_rep: "\<And>x. preorder.ideal r (rep x)"