proposition: Lemma CRuncountable : forall {R : ConstructiveReals} (un : nat -> CRcarrier R) (a b : CRcarrier R), a < b -> { x : CRcarrier R & prod (a < x < b) (forall n:nat, CRapart R x (un n)) }.
proof: Proof. intros. pose proof (CRlt_minus a b H). destruct (CR_cv_open_above (fun n:nat => CRpow (CR_of_Q R (1#2)) n) (b-a) 0) as [n nmaj]. apply GeoCvZero. exact H0. destruct (fun n:nat => OpenIntervalIntegrable a b H) as [intervInt intervMes]. destruct (RealSequenceCoverMeasure un n) as [coverInt coverMes]. specialize (nmaj n (Nat.le_refl n)). assert (0 < MeasureSet (IntegrableSetDifference _ _ intervInt coverInt)). { rewrite MeasureDifference. apply CRlt_minus. apply (CRle_lt_trans _ (MeasureSet coverInt)). apply IntegralNonDecreasing. intros x xdf xdg. simpl. destruct xdf, xdg. apply CRle_refl. 3: apply CRle_refl. 2: apply CRlt_asym, CRzero_lt_one. destruct a0. contradiction. apply (CRle_lt_trans _ _ _ coverMes). apply (CRlt_le_trans _ _ _ nmaj). rewrite intervMes. apply CRle_refl. } apply PositiveMeasureInhabited in H1. destruct H1 as [x xcv]. exists x. destruct xcv, H1. split. split. apply CRltEpsilon, H1. apply CRltEpsilon, H3. intro k. destruct (CRltLinear R). destruct (s (un k - CRpow (CR_of_Q R (1 # 2)) (2 + n + k)) x (un k-0)). - apply CRplus_lt_compat_l, CRopp_gt_lt_contravar. apply CRpow_gt_zero, CR_of_Q_pos. reflexivity. - destruct (s (un k) x (un k + CRpow (CR_of_Q R (1 # 2)) (2 + n + k))). + apply (CRle_lt_trans _ (un k + 0)). rewrite CRplus_0_r. apply CRle_refl. apply CRplus_lt_compat_l. apply CRpow_gt_zero, CR_of_Q_pos. reflexivity. + right. exact c0. + exfalso. apply H2. exists k. split. apply CRltForget. exact c. apply CRltForget. exact c0. - left. apply (CRlt_le_trans _ _ _ c). unfold CRminus. rewrite CRopp_0, CRplus_0_r. apply CRle_refl. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia