proposition: Lemma fcont_comp_le_compat : forall (D1 D2 D3:cpo) (f g : D2 -c> D3) (k l :D1-c> D2), f <= g -> k <= l -> f @_ k <= g @_ l.
proof: Proof. intros; apply fcont_le_intro; intro x. repeat (rewrite fcont_comp_simpl). apply Ole_trans with (g (k x)); auto. Qed.