proposition: Lemma Cauchy_prop2_prop : forall seq, Cauchy_prop2 seq -> Cauchy_prop seq.
proof: Proof. intros seq H. unfold Cauchy_prop in |- *. intros e H0. unfold Cauchy_prop2 in H. elim H. intro y; intros H1. unfold Cauchy_Lim_prop2 in H1. elim (H1 (e [/]TwoNZ)). intro N. intros H2. exists N. intros m H3. generalize (H2 _ H3); intro H4. generalize (le_n N); intro H5. generalize (H2 _ H5); intro H6. generalize (AbsSmall_minus _ _ _ _ H6); intro H7. generalize (AbsSmall_plus _ _ _ _ _ H4 H7); intro H8. rstepl (e [/]TwoNZ[+]e [/]TwoNZ). rstepr (seq m[-]y[+] (y[-]seq N)). assumption. apply pos_div_two. assumption. Qed.
imports: CoRN.reals.CReals Coq(Lia)