proposition: Lemma limsup_incr : forall f:natO-m>U, limsup f == lub f.
proof: Proof. unfold limsup; intros. apply Oeq_trans with (glb (fmon_cte natO (O2:=UI) (lub f))); auto. apply glb_eq_compat; apply fmon_eq_intro; simpl; intro. unfold fsup. apply (Oeq_trans (O:=UI)) with (lub (mseq_lift_left f n)). apply (Oeq_trans (O:=UI)) with (Ulub (mseq_lift_left f n)); auto. apply Oeq_sym; auto. Qed.
imports: ALEA(Utheory)