proposition: Lemma CSUCposPointApproxSequenceLength : forall n:nat, (y (CSUCposPointApproxSequence n) - x (CSUCposPointApproxSequence n) == (b-a) * CR_of_Q R (/2^Z.of_nat n)).
proof: Proof. induction n. - simpl. rewrite CRmult_1_r. reflexivity. - rewrite Nat2Z.inj_succ. unfold Z.succ. rewrite Qpower_plus. simpl. destruct (CSUCposPointApproxStep n (CSUCposPointApproxSequence n)); simpl. destruct a0, H0. unfold Qdiv. rewrite Qinv_mult_distr, CR_of_Q_mult, <- CRmult_assoc, <- IHn. clear IHn. exact H1. discriminate. Qed.
imports: QArith Qminmax Qpower Qabs ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructiveDiagonal ConstructivePartialFunctions ConstructiveUniformCont ConstructiveCauchyIntegral CMTbase CMTPositivity CMTIntegrableFunctions CMTFullSets CMTIntegrableSets