proposition: Lemma continuous_continuous2 : forall (D1 D2 D3:cpo) (F : D1-m>D2-M->D3), (forall k:D1, continuous (F k)) -> continuous F -> continuous2 F.
proof: Proof. red; intros. apply Ole_trans with (lub (F (lub f) @ g)); auto. apply lub_le; simpl; intros. apply Ole_trans with (lub ((F <_> (g n))@f)). apply Ole_trans with (lub (c:=D2 -M-> D3) (F@f) (g n)); auto. rewrite (lub_lift_right ((F @2 f) g) n). apply lub_le_compat; simpl; intros. apply Ole_trans with (F (f x) (g (x+n))); auto with arith. Qed.