proposition: Lemma Ulub_lub : forall f:natO-m>U, Ulub f == lub f.
proof: Proof. intros; unfold Ulub; apply lub_eq_compat; apply fmon_eq_intro; simpl; intros; auto. induction n; simpl; intros; auto. rewrite IHn; apply Ole_antisym; auto. Qed.
imports: ALEA(Utheory)