proposition: Lemma SigmaFiniteMonotone : forall {R : ConstructiveReals} (A : CRcarrier R -> Prop), let fn := fun n => @CharacFunc R _ (fun x => -CR_of_Q R (Z.of_nat n # 1) <= x /\ x <= CR_of_Q R (Z.of_nat n # 1) /\ A x) in forall n:nat, partialFuncLe (fn n) (fn (S n)).
proof: Proof. intros R A fn n x xdf xdg. simpl. destruct xdf. - destruct xdg. apply CRle_refl. exfalso. apply n0. destruct a, H0. repeat split. 3: exact H1. apply (CRle_trans _ (- CR_of_Q R (Z.of_nat n # 1))). apply CRopp_ge_le_contravar. apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le, le_S, Nat.le_refl. exact H. apply (CRle_trans _ (CR_of_Q R (Z.of_nat n # 1)) _ H0). apply CR_of_Q_le. unfold Qle, Qnum, Qden. do 2 rewrite Z.mul_1_r. apply Nat2Z.inj_le, le_S, Nat.le_refl. - destruct xdg. apply CRlt_asym, CRzero_lt_one. apply CRle_refl. Qed.
imports: QArith ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructivePower ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTFullSets CMTIntegrableSets CMTprofile