proposition: Lemma Cauchy_seq1_lft : Cauchy_prop seq1_lft.
proof: Proof. unfold Cauchy_prop in |- *. intro eps. intros H. assert ({ N : nat | Small[^]N[<=]eps}). apply (qi_yields_zero (Two[/]ThreeNZ) small_greater_zero small_less_one eps); auto. destruct X as [N H1]. exists N. intros. apply AbsSmall_leEq_trans with (seq1_rht N[-]seq1_lft N); auto. apply leEq_transitive with (Small[^]N); auto. apply intervals_smaller; auto. apply intervals_embed; auto. Qed.
imports: CoRN.reals.CReals1