proposition: Lemma liminf_le_compat : forall f g : nat -o> U, f <= g -> liminf f <= liminf g.
proof: Proof. unfold liminf; intros. apply lub_le_compat; simpl; intros; unfold finf; apply Uglb_le_compat; auto. Qed.
imports: ALEA(Utheory)