proposition: Lemma fixp_continuous : forall (D:cpo) (h : natO -m> (D-M->D)), (forall n, continuous (h n)) -> fixp (lub h) <= lub (Fixp D @ h).
proof: Proof. intros; unfold fixp. rewrite (iter_continuous_eq H). simpl; rewrite <- lub_exch_eq; auto. Qed.