proposition: Lemma Ulub_Uglb_exch_le : forall f : nat -> nat -> U, Ulub (fun n => Uglb (fun m => f n m)) <= Uglb (fun m => Ulub (fun n => f n m)).
proof: Proof. intros; apply le_Uglb; intro m. apply Ulub_le_compat; intro n. apply Uglb_le with (f:=fun m0 : nat => f n m0) (n:=m). Qed.
imports: ALEA(Utheory)