proposition: Lemma cont_lub : forall (D1 D2 : cpo) (f:natO -m> (D1 -m> D2)), (forall n, continuous (f n)) -> continuous (lub (c:=D1-M->D2) f).
proof: Proof. red; intros; simpl. apply Ole_trans with (lub (c:=D2) (Lub D2 @ (fmon_shift (double_app f h)))). apply lub_le_compat; intro n; simpl. apply Ole_trans with (lub ((f n) @ h)); auto. rewrite lub_exch_eq. apply lub_le_compat; intro n; simpl. apply lub_le_compat; intro m; simpl; auto. Qed.