proposition: Lemma limsup_le_compat : forall f g : nat -o> U, f <= g -> limsup f <= limsup g.
proof: Proof. unfold limsup; intros. apply glb_le_compat; simpl; intros; unfold fsup; apply Ulub_le_compat; auto. Qed.
imports: ALEA(Utheory)