proposition: Lemma CRuncountableDiag : forall {R : ConstructiveReals} (un : nat -> nat -> CRcarrier R) (a b : CRcarrier R), a < b -> { x : CRcarrier R & prod (a < x < b) (forall n k:nat, CRapart R x (un n k)) }.
proof: Proof. intros. destruct (CRuncountable (fun p:nat => let (n, k) := diagPlaneInv p in un n k) a b H). exists x. split. exact (fst p). intros n k. destruct p. specialize (c (diagPlane n k)). rewrite diagPlaneInject in c. exact c. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia