proposition: Lemma fcont_le_compat2 : forall (D1 D2 D3:cpo) (f : D1-c>D2-C->D3) (x y : D1) (z t : D2), x <= y -> z <= t -> f x z <= f y t.
proof: Proof. intros; apply Ole_trans with (f y z); unfold fconti_fun; auto. apply fmon_le_elim. apply (fmonotonic (Fcontit D2 D3) (x:=fcontit f x) (y:=fcontit f y)); auto. Qed.