proposition: Lemma BinarySubdivInside : forall {R : ConstructiveReals} (a b : CRcarrier R) (n i : nat), a <= b -> le i (2 ^ n) -> a <= BinarySubdiv a b n i <= b.
proof: Proof. split. - apply (CRle_trans _ (a+0)). rewrite CRplus_0_r. apply CRle_refl. apply CRplus_le_compat_l. apply CRmult_le_0_compat. apply CRmult_le_0_compat. apply CR_of_Q_le. destruct i; discriminate. rewrite <- (CRplus_opp_r a). apply CRplus_le_compat_r, H. apply CRpow_ge_zero. apply CR_of_Q_le. discriminate. - unfold BinarySubdiv. apply (CRplus_le_reg_l (-a)). rewrite <- CRplus_assoc, CRplus_opp_l, CRplus_0_l. rewrite (CRplus_comm (-a)), <- (CRmult_comm (b-a)), <- (CRmult_1_r (b+-a)). rewrite CRmult_assoc. apply CRmult_le_compat_l. rewrite <- (CRplus_opp_r a). apply CRplus_le_compat_r, H. apply (CRmult_le_reg_r (CRpow (CR_of_Q R 2) n)). apply CRpow_gt_zero, CR_of_Q_pos. reflexivity. rewrite CRmult_assoc, CRpow_mult. rewrite (CRpow_proper (CR_of_Q R (/ 2) * CR_of_Q R 2) 1). rewrite CRpow_one, CRmult_1_r, CRmult_1_l. apply (CRle_trans _ (CR_of_Q R (Z.of_nat (2^n)#1))). apply CR_of_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_r, Z.mul_1_r. apply Nat2Z.inj_le, H0. rewrite <- (pow_nat 2). apply CRle_refl. 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