proposition: Lemma CRealComplete : forall xn : nat -> CReal, (forall p : positive, {n : nat | forall i j : nat, (n <= i)%nat -> (n <= j)%nat -> (CReal_abs (xn i + - xn j)) <= (inject_Q (1 # p))}) -> {l : CReal & forall p : positive, {n : nat | forall i : nat, (n <= i)%nat -> (CReal_abs (xn i + - l)) <= (inject_Q (1 # p))}}.
proof: Proof. intros. destruct (Rcauchy_complete xn) as [l cv]. - intro p. destruct (H p) as [n a]. exists n. intros. exact (a i j H0 H1). - exists l. intros p. destruct (cv p). exists x. exact c. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra Qminmax