proposition: Lemma iter_continuous : forall (D:cpo), forall h : natO -m> (D-M->D), (forall n, continuous (h n)) -> iter (lub h) <= lub (Iter D @ h).
proof: Proof. red; intros; intro k. induction k; auto. rewrite iterS_simpl. apply Ole_trans with (lub h (lub (c:=natO -M-> D) (Iter D @ h) k)); auto. repeat (rewrite fmon_lub_simpl). apply Ole_trans with (lub (c:=D) (lub (c:=natO-M->D) (double_app h ((Iter D @ h) <_> k)))). apply lub_le_compat; simpl; intros. apply Ole_trans with (lub ((h x)@((Iter D @ h) <_> k))); auto. apply Ole_trans with (lub (fmon_diag (double_app h ((Iter D @ h) <_> k)))); auto. case (double_lub_diag (double_app h ((Iter D @ h) <_> k))); intros L _. apply Ole_trans with (1:=L); auto. Qed.