proposition: Lemma continuous_eq_compat : forall (D1 D2 : cpo) (f g:D1 -m> D2), f==g -> continuous f -> continuous g.
proof: Proof. red; intros. apply Ole_trans with (f (lub h)). assert (g <= f); auto. rewrite <- H; auto. Qed.