proposition: Lemma CRuncountableDiag3 : forall {R : ConstructiveReals} (un : nat -> nat -> nat -> CRcarrier R) (a b : CRcarrier R), a < b -> { x : CRcarrier R & prod (a < x < b) (forall n k i:nat, CRapart R x (un n k i)) }.
proof: Proof. intros. destruct (CRuncountableDiag (fun p i:nat => let (n, k) := diagPlaneInv p in un n k i) a b H). exists x. split. exact (fst p). intros n k i. destruct p. specialize (c (diagPlane n k) i). 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