proposition: Lemma Rcauchy_limit : forall (xn : nat -> CReal) (xcau : Un_cauchy_mod xn), QCauchySeqLin (fun n : positive => let (p, _) := xcau (4 * n)%positive in seq (xn p) (4 * Z.neg n)%Z).
proof: Proof. intros xn xcau n p q Hp Hq. destruct (xcau (4 * p)%positive) as [i imaj], (xcau (4 * q)%positive) as [j jmaj]. assert (CReal_abs (xn i - xn j) <= inject_Q (1 # 4 * n)). { destruct (le_lt_dec i j). - apply (CReal_le_trans _ _ _ (imaj i j (Nat.le_refl _) l)). apply inject_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos.mul_le_mono_l, Hp. - apply le_S, le_S_n in l. apply (CReal_le_trans _ _ _ (jmaj i j l (Nat.le_refl _))). apply inject_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos.mul_le_mono_l, Hq. } clear jmaj imaj. setoid_replace (1#n)%Q with ((1#(3*n)) + ((1#(3*n)) + (1#(3*n))))%Q. 2: rewrite Qinv_plus_distr, Qinv_plus_distr; reflexivity. apply lt_inject_Q. rewrite inject_Q_plus. rewrite Qabs_Rabs. apply (CReal_le_lt_trans _ (CReal_abs (inject_Q (seq (xn i) (4 * Z.neg p)%Z) - xn i) + CReal_abs (xn i - inject_Q(seq (xn j) (4 * Z.neg q)%Z)))). - unfold Qminus. rewrite inject_Q_plus, opp_inject_Q. setoid_replace (inject_Q (seq (xn i) (4 * Z.neg p)%Z) + - inject_Q (seq (xn j) (4 * Z.neg q)%Z)) with (inject_Q (seq (xn i) (4 * Z.neg p)%Z) - xn i + (xn i - inject_Q (seq (xn j) (4 * Z.neg q)%Z))). 2: ring. apply CReal_abs_triang. - apply CReal_plus_le_lt_compat. + rewrite CReal_abs_minus_sym. apply (CReal_le_trans _ (inject_Q (1# 4*p))). * apply CReal_cv_self. * apply inject_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos. apply (Pos.le_trans _ (4*n)). -- apply Pos.mul_le_mono_r. discriminate. -- apply Pos.mul_le_mono_l. exact Hp. + apply (CReal_le_lt_trans _ (CReal_abs (xn i - xn j + (xn j - inject_Q (seq (xn j) (4 * Z.neg q)%Z))))). * apply CReal_abs_morph. ring. * apply (CReal_le_lt_trans _ _ _ (CReal_abs_triang _ _)). rewrite inject_Q_plus. apply CReal_plus_le_lt_compat. -- apply (CReal_le_trans _ _ _ H). apply inject_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos. apply Pos.mul_le_mono_r. discriminate. -- apply (CReal_le_lt_trans _ (inject_Q (1#4*q))). ++ apply CReal_cv_self. ++ apply inject_Q_lt. unfold Qlt, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_lt_pos. apply (Pos.lt_le_trans _ (4*n)). ** apply Pos.mul_lt_mono_r. reflexivity. ** apply Pos.mul_le_mono_l. exact Hq. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra