proposition: Lemma iter_continuous_eq : forall (D:cpo), forall h : natO -m> (D-M->D), (forall n, continuous (h n)) -> iter (lub h) == lub (Iter D @ h).
proof: Proof. intros; apply Ole_antisym; auto. exact (lub_comp_le (Iter D) h). Qed.