proposition: Lemma FindInterval {R : ConstructiveReals} (un : nat -> CRcarrier R) (x : CRcarrier R) (i j : nat) : (forall n:nat, un n <= un (S n)) -> (forall n:nat, CRapart R x (un n)) -> un i < x < un j -> { k : nat & un k < x < un (S k) }.
proof: Proof. intro uIncr. assert (forall b : nat, un O <= un b). { induction b. apply CRle_refl. apply (CRle_trans _ (un b) _ IHb). apply uIncr. } induction j. - intros. pose proof (CRlt_trans _ _ _ (fst H1) (snd H1)) as H3. contradict H3. apply H. - intros. specialize (IHj H0). destruct (H0 j). exact (IHj (pair (fst H1) c)). exists j. exact (pair c (snd H1)). Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveSum ConstructivePower ConstructiveAbs ConstructiveMinMax ConstructiveLimits ConstructiveUniformCont ConstructivePartialFunctions ConstructiveDiagonal CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTReals Lia