proposition: Lemma lub_exch_le : forall (D:cpo) (h : natO -m> (natO -m> D)), lub (Lub D @ h) <= lub (lub_fun h).
proof: Proof. intros; apply lub_le; intros; simpl. apply lub_le; intros. apply Ole_trans with (lub (h n)); auto. apply lub_le_compat; intro. unfold lub_fun; simpl. apply le_lub with (f:=h <_> x) (n:=n). Qed.