proposition: Lemma Rcomplete : forall xn : nat -> R, (forall p : positive, {n : nat | forall i j : nat, (n <= i)%nat -> (n <= j)%nat -> IQR (1 # p) < Rabst (CReal_abs (Rrepr (xn i + - xn j))) -> False}) -> {l : R & forall p : positive, {n : nat | forall i : nat, (n <= i)%nat -> IQR (1 # p) < Rabst (CReal_abs (Rrepr (xn i + - l))) -> False}}.
proof: Proof. intros. destruct (Rcauchy_complete (fun n => Rrepr (xn n))) as [l llim]. - intro p. specialize (H p) as [n nmaj]. exists n. intros. specialize (nmaj i j H H0). unfold IQR in nmaj. intro abs. apply nmaj. rewrite Rlt_def. apply CRealLtForget. rewrite Rquot2, Rquot2. apply (CReal_lt_le_trans _ _ _ abs). rewrite Rrepr_plus, Rrepr_opp. apply CRealLe_refl. - exists (Rabst l). intros. specialize (llim p) as [n nmaj]. exists n. intros. specialize (nmaj i H0). unfold IQR in H1. apply nmaj. rewrite Rlt_def in H1. apply CRealLtEpsilon in H1. rewrite Rquot2, Rquot2 in H1. apply (CReal_lt_le_trans _ _ _ H1). rewrite Rrepr_plus, Rrepr_opp, Rquot2. apply CRealLe_refl. Qed.
imports: QArith_base Rdefinitions Raxioms ConstructiveReals ConstructiveCauchyReals ConstructiveCauchyRealsMult ConstructiveRcomplete ConstructiveCauchyAbs ConstructiveRealsMorphisms