proposition: Lemma BinarySubdivIncr : forall {R : ConstructiveReals} (a b : CRcarrier R) (n i : nat), 0 < a < b -> 0 < BinarySubdiv a b n i < BinarySubdiv a b n (S i).
proof: Proof. intros. assert (0 < (b - a) * CRpow (CR_of_Q R (/ 2)) n). { apply CRmult_lt_0_compat. apply CRlt_minus. exact (snd H). apply CRpow_gt_zero. apply CR_of_Q_pos. reflexivity. } split. - unfold BinarySubdiv. apply (CRlt_le_trans _ (a + 0)). rewrite CRplus_0_r. exact (fst H). apply CRplus_le_compat_l. rewrite CRmult_assoc. apply CRmult_le_0_compat. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Zle_0_nat. apply CRlt_asym, H0. - apply CRplus_lt_compat_l. apply CRmult_lt_compat_r. apply CRpow_gt_zero, CR_of_Q_pos. reflexivity. apply CRmult_lt_compat_r. apply CRlt_minus. exact (snd H). apply CR_of_Q_lt. unfold Qlt, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply inj_lt, Nat.le_refl. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia