proposition: Lemma continuous_comp : forall (D1 D2 D3:cpo) (f:D2-m>D3)(g:D1-m>D2), continuous f -> continuous g -> continuous (f@g).
proof: Proof. red; intros. rewrite fmon_comp_simpl. apply Ole_trans with (f (lub (g@h))); auto. apply Ole_trans with (lub (f@(g@h))); auto. Qed.