proposition: Lemma StepApproxCv : forall {R : ConstructiveReals} (t : CRcarrier R), CR_cv R (fun n => t*CR_of_Q _ (1-(1#Pos.of_nat (2*S n)))) t.
proof: Proof. intros. apply (CR_cv_proper _ (1*t)). 2: apply CRmult_1_l. apply (CR_cv_eq _ (fun n : nat => CR_of_Q R (1 - (1 # Pos.of_nat (2 * S n))) * t)). intro n. apply CRmult_comm. apply CR_cv_scale. intro p. exists (Pos.to_nat p). intros. setoid_replace (CR_of_Q R (1 - (1 # Pos.of_nat (2 * S i))) - 1) with (-CR_of_Q R (1 # Pos.of_nat (2 * S i))). - rewrite CRabs_opp, CRabs_right. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_l. apply Pos2Z.pos_le_pos. rewrite Pos2Nat.inj_le, Nat2Pos.id. 2: discriminate. apply (Nat.le_trans _ _ _ H). simpl. apply le_S. apply (Nat.le_trans _ (i+0)). rewrite Nat.add_comm. apply Nat.le_refl. apply Nat.add_le_mono_l, Nat.le_0_l. apply CR_of_Q_le. discriminate. - unfold Qminus. rewrite CR_of_Q_plus, CR_of_Q_opp. unfold CRminus. rewrite CRplus_comm, <- CRplus_assoc, CRplus_opp_l. rewrite CRplus_0_l. reflexivity. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia