proposition: Lemma limsup_le_plus : forall (f g: nat -> U), limsup (fun x => f x + g x) <= limsup f + limsup g.
proof: Proof. intros; unfold limsup,fplus. apply Ole_trans with (glb ((Imon2 UPlus @2 (Fsup f)) (Fsup g))). apply glb_le_compat; simpl; intro. unfold fsup; auto. rewrite glb_eq_plus; auto. Qed.
imports: ALEA(Utheory)