add lemma iterate_below_fix

--- a/src/HOLCF/Fix.thy	Sat Feb 06 16:32:34 2010 +0100
+++ b/src/HOLCF/Fix.thy	Sun Feb 07 10:15:15 2010 -0800
@@ -73,6 +73,10 @@
 apply simp
 done
 
+lemma iterate_below_fix: "iterate n\<cdot>f\<cdot>\<bottom> \<sqsubseteq> fix\<cdot>f"
+  unfolding fix_def2
+  using chain_iterate by (rule is_ub_thelub)
+
 text {*
   Kleene's fixed point theorems for continuous functions in pointed
   omega cpo's