proposition: Lemma has_limit_cauchy : forall f l, is_limit f l -> cauchy f.
proof: Proof. unfold cauchy,is_limit; intros. apply (H (S p)); clear H; auto; intros M H; apply exc_intro with M; intros n m H1; unfold limsup. case (H n); auto with arith; intros. case (H m); auto with arith; intros. apply Ole_trans with (l + [1/2]^(S p)); auto. apply Ole_trans with (f m + [1/2]^(S p) + [1/2]^(S p)); auto. norm_assoc_right; Usimpl; auto. Qed.
imports: ALEA(Utheory)