proposition: Lemma liminf_le_plus : forall (f g: nat -> U), liminf f + liminf g <= liminf (fun x => f x + g x).
proof: Proof. intros; unfold liminf,fplus. apply Ole_trans with (lub ((UPlus @2 (Finf f)) (Finf g))); auto. apply lub_le_compat; simpl; unfold finf; auto. Qed.
imports: ALEA(Utheory)