proposition: Lemma cauchy_lim : forall f, cauchy f -> is_limit f (limsup f).
proof: Proof. unfold cauchy,is_limit; intros. apply (H p); clear H; auto; intros M H; apply exc_intro with M; intros n H1; unfold limsup; split. apply Ole_trans with (glb ((Imon (UPlus <_> [1/2]^p)) @ (mseq_lift_left (Fsup f) M))). apply le_glb; simpl; intro k. apply Ole_trans with (f (M + k)%nat + [1/2]^p); auto with arith. rewrite glb_eq_plus_cte_right; Usimpl. rewrite <- glb_lift_left; auto. apply Ole_trans with (Fsup f M); auto; simpl. unfold fsup; apply Ulub_le; intro k; auto with arith. Qed.
imports: ALEA(Utheory)