proposition: Lemma CSUCposPointApproxLimitNested : forall n : nat, let (l,_) := CSUCposPointApproxSequenceCauchy in x (CSUCposPointApproxSequence n) <= l /\ l <= y (CSUCposPointApproxSequence n).
proof: Proof. intro n. pose proof (CSUCposPointApproxSequenceNested n). destruct CSUCposPointApproxSequenceCauchy as [l lcv], (CSUCposPointApproxSequence n); simpl. split. - apply (CR_cv_bound_down (fun n : nat => x (CSUCposPointApproxSequence n)) _ _ n). intros. destruct (Nat.le_exists_sub n n0 H0). destruct H1. subst n0. rewrite Nat.add_comm. specialize (H x1). destruct (CSUCposPointApproxSequence (n + x1)); simpl; simpl in H. apply H. apply lcv. - apply (CR_cv_bound_up (fun n : nat => x (CSUCposPointApproxSequence n)) _ _ n). intros. destruct (Nat.le_exists_sub n n0 H0). destruct H1. subst n0. rewrite Nat.add_comm. specialize (H x1). destruct (CSUCposPointApproxSequence (n + x1)); simpl; simpl in H. apply (CRle_trans _ y1). exact lexy1. apply H. apply lcv. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets