proposition: Lemma cauchy_prop_cauchy_crit : (CauchySeq ROrdField) -> forall s : (nat -> ROrdField), (Cauchy_prop (R:=ROrdField) s) -> (Rseries.Cauchy_crit s).
proof: Proof. intros x seq cprop. unfold Cauchy_prop in cprop. unfold Rseries.Cauchy_crit. intros eps epsgt. elim (cprop ((eps / 2 / 2)%R) (eps2_Rgt_R0 _ (eps2_Rgt_R0 _ epsgt))). intros N NProp. exists N. intros n m ngt mgt. assert (AbsSmall (eps / 2) ((seq n) - (seq m)) )%R. stepr ((seq n - seq N) + (seq N - seq m))%R. stepl (eps / 2 / 2 + eps / 2 / 2)%R. apply AbsSmall_plus. apply NProp; assumption. apply (AbsSmall_minus). apply NProp; assumption. simpl; field. simpl; ring. destruct H. unfold Rfunctions.R_dist. apply Rabs_def1. clear - H0 epsgt. simpl in *. lra. clear - H epsgt. simpl in *. lra. Qed.
imports: CoRN.algebra.CSetoids CoRN.algebra.CSemiGroups CoRN.algebra.CMonoids CoRN.algebra.CGroups CoRN.tactics.CornTac CoRN.algebra.CAbGroups CoRN.algebra.CRings CoRN.algebra.CFields CoRN.algebra.COrdFields CoRN.reals.CReals Coq.Reals.RIneq Coq.Reals.Rcomplete Coq.Reals.Rlimit Coq.Reals.Rbasic_fun Coq(Lra)