proposition: Lemma le_Uglb: forall (f : nat -> U) (x:U), (forall n : nat, x <= f n)-> x <= Uglb f.
proof: Proof. unfold Uglb; intros; apply Uinv_le_perm_right. apply Ulub_le with (f:=fun n => [1-]f n); auto. Qed.
imports: ALEA(Utheory)