proposition: Lemma Ulub_eq_esp_right : forall (f : nat -> U) (k : U), Ulub (fun n => f n & k) == Ulub f & k.
proof: Proof. intros; apply Ole_antisym. apply Ulub_le; auto. apply Uplus_inv_le_esp. apply Ole_trans with (Ulub (fun n => (f n & k) + ([1-]k))); auto. Qed.
imports: ALEA(Utheory)