proposition: Lemma CReal_from_cauchy_cauchy : forall (xn : nat -> CReal) (xcau : Un_cauchy_mod xn), QCauchySeq (CReal_from_cauchy_seq xn xcau).
proof: Proof. intros xn xcau n p q Hp Hq. remember (CReal_from_cauchy_cm n) as n'. remember (CReal_from_cauchy_cm p) as p'. remember (CReal_from_cauchy_cm q) as q'. unfold CReal_from_cauchy_seq. rewrite <- Heqp', <- Heqq'. destruct (xcau (4 * 2^p')%positive) as [i imaj]. destruct (xcau (4 * 2^q')%positive) as [j jmaj]. assert (CReal_abs (xn i - xn j) <= inject_Q (1 # 4 * 2^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. subst; apply Pos.mul_le_mono_l, Pos_pow_le_mono_r, CReal_from_cauchy_cm_mono, 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. subst; apply Pos.mul_le_mono_l, Pos_pow_le_mono_r, CReal_from_cauchy_cm_mono, Hq. } clear jmaj imaj. setoid_replace (2^n)%Q with ((1#3)*2^n + ((1#3)*2^n + (1#3)*2^n))%Q by ring. apply lt_inject_Q. rewrite inject_Q_plus. rewrite Qabs_Rabs. apply (CReal_le_lt_trans _ (CReal_abs (inject_Q (seq (xn i) (Z.neg p' - 2)%Z) - xn i) + CReal_abs (xn i - inject_Q(seq (xn j) (Z.neg q' - 2)%Z)))). { unfold Qminus. rewrite inject_Q_plus, opp_inject_Q. setoid_replace (inject_Q (seq (xn i) (Z.neg p' - 2)%Z) + - inject_Q (seq (xn j) (Z.neg q' - 2)%Z)) with (inject_Q (seq (xn i) (Z.neg p' - 2)%Z) - xn i + (xn i - inject_Q (seq (xn j) (Z.neg q' - 2)%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)*2^(Z.neg p')))). - change (1#4)%Q with ((1#2)^2)%Q. rewrite Qmult_comm, <- Qpower_minus_pos. apply CReal_cv_self'. - apply inject_Q_le. apply Qmult_le_compat_nonneg. + lra. + { split. - apply Qpower_pos; lra. - apply Qpower_le_compat_l. + subst; unfold CReal_from_cauchy_cm; destruct p; lia. + lra. } } apply (CReal_le_lt_trans _ (CReal_abs (xn i - xn j + (xn j - inject_Q (seq (xn j) (Z.neg q' - 2)%Z))))). 1: 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. rewrite Qmult_frac_l. rewrite <- (Z.pow_1_l (Z.pos n')) at 2 by lia. rewrite <- (Qpower_decomp_pos). change (1#2)%Q with (/2)%Q; rewrite Qinv_power, <- Qpower_opp. apply Qmult_le_compat_nonneg. - lra. - { split. - apply Qpower_pos; lra. - apply Qpower_le_compat_l. + subst; unfold CReal_from_cauchy_cm; destruct n; lia. + lra. } } apply (CReal_le_lt_trans _ (inject_Q ((1#4)*2^(Z.neg q')))). { change (1#4)%Q with ((1#2)^2)%Q. rewrite Qmult_comm, <- Qpower_minus_pos. apply CReal_cv_self'. } apply inject_Q_lt. setoid_rewrite Qmult_comm at 1 2. apply Qmult_le_lt_compat_pos. + { split. - apply Qpower_0_lt; lra. - apply Qpower_le_compat_l. + subst; unfold CReal_from_cauchy_cm. destruct q; lia. + lra. } + lra. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra