proposition: Lemma continuous2_comp : forall (D1 D2 D3 D4:cpo) (f:D1-m>D2)(g:D2-m>D3-M->D4), continuous f -> continuous2 g -> continuous2 (g @ f).
proof: Proof. intros; apply continuous_continuous2; auto. red; intros. rewrite fmon_comp_simpl. apply (continuous2_right (F:=g) (f k) h); trivial. Qed.