proposition: Lemma BinarySubdivRight : forall {R : ConstructiveReals} (a b : CRcarrier R) (n : nat), a <= b -> BinarySubdiv a b n (2 ^ n) == b.
proof: Proof. intros. unfold BinarySubdiv. apply (CRplus_eq_reg_l (-a)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l, (CRplus_comm (-a)). rewrite <- (CRmult_comm (b-a)), <- (CRmult_1_r (b+-a)). rewrite CRmult_assoc. apply CRmult_morph. reflexivity. apply (CRmult_eq_reg_r (CRpow (CR_of_Q R 2) n)). left. apply CRpow_gt_zero, CR_of_Q_pos. reflexivity. rewrite CRmult_assoc, CRmult_1_l, CRpow_mult. rewrite (CRpow_proper (CR_of_Q R (/ 2) * CR_of_Q R 2) 1). rewrite CRpow_one, CRmult_1_r. apply (pow_nat 2). rewrite <- CR_of_Q_mult. apply CR_of_Q_morph. reflexivity. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia