proposition: Lemma Cauchy_prop1_prop : forall seq, Cauchy_prop1 seq -> Cauchy_prop seq.
proof: Proof. intros seq H. unfold Cauchy_prop1 in H. unfold Cauchy_prop in |- *. intros. cut (e [#] [0]). intro eNZ. elim (Archimedes ([1][/] e[//]eNZ)). intros x H1. elim (H x). intros x0 H2. split with x0. intros m H3. generalize (H2 _ H3). intro. apply AbsSmall_leEq_trans with (one_div_succ (R:=IR) x). unfold one_div_succ in |- *. unfold Snring in |- *. apply shift_div_leEq'. apply nring_pos. auto with arith. astepr (e[*]nring (S x)). apply leEq_transitive with (e[*]nring x). apply shift_leEq_mult' with eNZ. assumption. assumption. apply less_leEq. apply mult_resp_less_lft. apply nring_less. auto. assumption. assumption. apply pos_ap_zero. assumption. Qed.
imports: CoRN.reals.CReals Coq(Lia)