proposition: Lemma CSUCposPointApproxSequenceCvZero : forall n : positive, { p : nat & forall i : nat, (p <= i)%nat -> CRabs R (y (CSUCposPointApproxSequence i) - x (CSUCposPointApproxSequence i)) < CR_of_Q R (1 # n) }.
proof: Proof. intros n. destruct (CRup_nat (b - a)) as [i imaj]. destruct i. exfalso. simpl in imaj. rewrite <- (CRplus_opp_r a) in imaj. apply CRplus_lt_reg_r in imaj. contradiction. destruct (@GeoCvZero R (Pos.of_nat (S i)*n)%positive) as [p pmaj]. exists p. intros. apply (CRle_lt_trans _ ((b-a)* CR_of_Q R ((/2)^Z.of_nat p))). - rewrite Qinv_power. pose proof (CSUCposPointApproxSequenceLength p). rewrite <- H0. clear H0. destruct (Nat.le_exists_sub p i0 H), H0. subst i0. 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. apply (CRle_trans _ (x (CSUCposPointApproxSequence (x0+p)))). rewrite Nat.add_comm. apply CSUCposPointApproxSequenceNested. destruct (CSUCposPointApproxSequence (x0 + p)); simpl. exact lexy0. rewrite Nat.add_comm. apply CSUCposPointApproxSequenceNested. - specialize (pmaj p (Nat.le_refl p)). unfold CRminus in pmaj. rewrite CRopp_0, CRplus_0_r in pmaj. apply (CRlt_le_trans _ (CR_of_Q R ((Z.of_nat (S i) # 1) * (/ 2) ^ Z.of_nat p ))). rewrite CR_of_Q_mult. apply CRmult_lt_compat_r. 2: exact imaj. apply CR_of_Q_pos. apply Qpower_positive. reflexivity. rewrite CRabs_right in pmaj. 2: apply CRlt_asym, CRpow_gt_zero; exact Rlt_0_half. apply CR_of_Q_le. setoid_replace (CRpow (CR_of_Q R (1 # 2)) p) with (CR_of_Q R ((/ 2) ^ Z.of_nat p )) in pmaj. destruct (Q_dec ((/ 2) ^ Z.of_nat p) (1 # Pos.of_nat (S i) * n)). destruct s. apply (Qmult_lt_l _ _ (Z.of_nat (S i) # 1)) in q. apply (Qle_trans _ ((Z.of_nat (S i) # 1) * (1 # Pos.of_nat (S i) * n))%Q). apply Qlt_le_weak, q. 2: reflexivity. unfold Qmult, Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_l, Pos.mul_1_l. rewrite Pos2Z.inj_mul. unfold Z.of_nat. rewrite Pos.of_nat_succ. apply Z.le_refl. exfalso. apply (CR_of_Q_lt R) in q. apply pmaj, q. rewrite q. unfold Qmult, Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_l, Pos.mul_1_l. rewrite Pos2Z.inj_mul. unfold Z.of_nat. rewrite Pos.of_nat_succ. apply Z.le_refl. rewrite pow_inject_Q. reflexivity. discriminate. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets