proposition: Lemma CSUCposPointApproxSequenceCauchy : { l : CRcarrier R & CR_cv R (fun n => x (CSUCposPointApproxSequence n)) l }.
proof: Proof. apply (CR_complete R (fun n => x (CSUCposPointApproxSequence n))). intros n. destruct (CSUCposPointApproxSequenceCvZero n) as [p pmaj]. exists p. intros. apply (CRle_trans _ (y (CSUCposPointApproxSequence p) - x (CSUCposPointApproxSequence p))). - destruct (Nat.le_exists_sub p j H0), H1. subst j. destruct (Nat.le_exists_sub p i H), H1. subst i. apply Rsmaller_interval. rewrite Nat.add_comm. apply CSUCposPointApproxSequenceNested. apply (CRle_trans _ (y (CSUCposPointApproxSequence (x0 + p)))). destruct (CSUCposPointApproxSequence (x0 + p)); simpl. exact lexy0. rewrite Nat.add_comm. apply CSUCposPointApproxSequenceNested. rewrite Nat.add_comm. apply CSUCposPointApproxSequenceNested. apply (CRle_trans _ (y (CSUCposPointApproxSequence (x1 + p)))). destruct (CSUCposPointApproxSequence (x1 + p)); simpl. exact lexy0. rewrite Nat.add_comm. apply CSUCposPointApproxSequenceNested. - specialize (pmaj p (Nat.le_refl p)). unfold CRminus in pmaj. unfold CRminus. apply CRlt_asym. exact (CRle_lt_trans _ _ _ (CRle_abs _) pmaj). Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets