proposition: Lemma StepApproxBetween : forall {R : ConstructiveReals} (t : CRcarrier R) (tPos : 0 < t) (n : nat), 0 < t*CR_of_Q _ (1-(1#Pos.of_nat (2*S n))) < t.
proof: Proof. split. - apply CRmult_lt_0_compat. exact tPos. apply CR_of_Q_pos. unfold Qminus. rewrite <- (Qplus_opp_r (1 # Pos.of_nat (2 * S n))), Qplus_lt_l. unfold Qlt, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_lt_pos. rewrite Pos2Nat.inj_lt, Nat2Pos.id. simpl. apply le_n_S. rewrite Nat.add_comm. apply le_n_S, Nat.le_0_l. discriminate. - apply (CRlt_le_trans _ (t* CR_of_Q _ 1)). 2: rewrite CRmult_1_r; apply CRle_refl. apply CRmult_lt_compat_l. exact tPos. apply CR_of_Q_lt. apply (Qplus_lt_l _ _ ((1 # Pos.of_nat (2 * S n))-1)). ring_simplify. reflexivity. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia