proposition: Lemma CRcauchy_complete : forall xn : nat -> CR, CRcauchy_sequence xn -> {l : CR & forall p : positive, {n : nat | forall i : nat, (n <= i)%nat -> (' (1 # p) < CRabs (xn i - l))%CR -> False}}.
proof: Proof. intros xn xncau. exists (Cjoin_fun (Build_RegularFunction (CRstandard_regular xn xncau))). intro p. exists (proj1_sig (xncau (2*p)%positive)). intros i H. apply CRle_not_lt. apply (CRle_trans (CRdistance_triangle _ (CRstandard_modulus xn xncau (Qpos2QposInf (1#2*p))) _)). apply (@CRle_trans _ ('(1#2*p) + '(1#2*p))%CR). apply CRplus_le_compat. - simpl. destruct (xncau (2*p)%positive) as [n H0] eqn:des. apply CRle_not_lt. apply H0. exact H. clear H i. simpl in des. rewrite des. apply Nat.le_refl. - apply CRabs_ball, ball_sym. apply (Cjoin_ball (Build_RegularFunction (CRstandard_regular xn xncau)) (1#2*p)). - rewrite CRplus_Qplus. apply CRle_Qle. rewrite Qinv_plus_distr. apply Z.le_refl. Qed.
imports: Coq.Reals.Abstract.ConstructiveReals CoRN.model.metric2.Qmetric CoRN.model.metric2.CRmetric CoRN.reals.fast.CRFieldOps CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.model.totalorder.QposMinMax Coq.Logic.ConstructiveEpsilon