proposition: Lemma BinarySubdivNext : forall {R : ConstructiveReals} (a b : CRcarrier R) (n i:nat), BinarySubdiv a b n i + CRpow (CR_of_Q R (1 # 2)) n * (b - a) == BinarySubdiv a b n (S i).
proof: Proof. intros. unfold BinarySubdiv. rewrite CRplus_assoc. apply CRplus_morph. reflexivity. rewrite CRmult_assoc, <- (CRmult_comm (b-a)). rewrite <- (CRmult_1_l ((b - a) * CRpow (CR_of_Q R (1 # 2)) n)). rewrite (CRpow_proper (CR_of_Q R (/ 2)) (CR_of_Q R (1#2))). 2: apply CR_of_Q_morph; reflexivity. rewrite <- CRmult_plus_distr_r. rewrite CRmult_assoc. apply CRmult_morph. 2: reflexivity. rewrite <- CR_of_Q_plus. apply CR_of_Q_morph. rewrite Qinv_plus_distr. unfold Qeq, Qnum, Qden. do 2 rewrite Z.mul_1_r. replace 1%Z with (Z.of_nat 1). rewrite <- Nat2Z.inj_add. rewrite Nat.add_comm. reflexivity. reflexivity. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia