proposition: Lemma Rcauchy_complete : forall (xn : nat -> CReal), Un_cauchy_mod xn -> { l : CReal & seq_cv xn l }.
proof: Proof. intros xn cau. exists (CReal_from_cauchy xn cau). intro p. pose proof (CReal_cv_self' (CReal_from_cauchy xn cau) (Z.neg p - 1)%Z) as H. pose proof (cau (2*p)%positive) as [k cv]. rewrite CReal_abs_minus_sym in H. unfold CReal_from_cauchy at 1 in H. rewrite CReal_red_seq in H. unfold CReal_from_cauchy_seq in H. remember (CReal_from_cauchy_cm (Z.neg p - 1))%positive as i'. destruct (cau (4 * 2 ^ i')%positive) as [i imaj]. exists (max k i). intros j H0. setoid_replace (xn j - CReal_from_cauchy xn cau) with (xn j - inject_Q (seq (xn i) (Z.neg i' - 2)%Z) + (inject_Q (seq (xn i) (Z.neg i' - 2)%Z) - CReal_from_cauchy xn cau)). 2: ring. apply (CReal_le_trans _ _ _ (CReal_abs_triang _ _)). apply (CReal_le_trans _ (inject_Q (1#2*p) + inject_Q (1#2*p))). - apply CReal_plus_le_compat. 2: { apply (CReal_le_trans _ _ _ H). apply inject_Q_le. rewrite Qpower_minus_pos. assert(forall (n:Z) (p q : positive), n#(p*q) == (n#p) * (1#q))%Q as Aux by ( intros; unfold Qeq, Qmult, Qnum, Qden; ring ); rewrite Aux; clear Aux. rewrite Qmult_comm; apply Qmult_le_l; [lra|]. pose proof Qpower_2powneg_le_inv p. pose proof Qpower_0_lt 2 (Z.neg p)%Z; lra. } specialize (imaj j i (Nat.le_trans _ _ _ (Nat.le_max_r _ _) H0) (Nat.le_refl _)). apply (CReal_le_trans _ (inject_Q (1 # 4 * p) + inject_Q (1 # 4 * p))). + setoid_replace (xn j - inject_Q (seq (xn i) (Z.neg i' - 2))) with (xn j - xn i + (xn i - inject_Q (seq (xn i) (Z.neg i' - 2)))). 2: ring. apply (CReal_le_trans _ _ _ (CReal_abs_triang _ _)). apply CReal_plus_le_compat. * apply (CReal_le_trans _ _ _ imaj). rewrite Heqi'. change (Z.neg p - 1)%Z with (Z.neg (p + 1))%Z. unfold CReal_from_cauchy_cm. apply inject_Q_le. unfold Qle, Qnum, Qden. rewrite Z.mul_1_l, Z.mul_1_l. apply Pos2Z.pos_le_pos, Pos.mul_le_mono_l. pose proof Pospow_lin_le_2pow p. rewrite Pos.add_1_r, Pos.pow_succ_r. lia. * clear imaj. pose proof CReal_cv_self' (xn i) (Z.neg i' - 2). apply (CReal_le_trans _ _ _ H1). apply inject_Q_le. rewrite Heqi'. change (Z.neg p - 1)%Z with (Z.neg (p + 1))%Z. unfold CReal_from_cauchy_cm. change (Z.neg (p + 1))%Z with (Z.neg p - 1)%Z. ring_simplify (Z.neg p - 1 - 2)%Z. rewrite Qpower_minus_pos. assert(forall (n:Z) (p q : positive), n#(p*q) == (n#p) * (1#q))%Q as Aux by ( intros; unfold Qeq, Qmult, Qnum, Qden; ring ); rewrite Aux; clear Aux. pose proof Qpower_2powneg_le_inv p. pose proof Qpower_0_lt 2 (Z.neg p)%Z; lra. + rewrite <- inject_Q_plus. rewrite (inject_Q_morph _ (1#2*p)). * apply CRealLe_refl. * rewrite Qinv_plus_distr; reflexivity. - rewrite <- inject_Q_plus. rewrite (inject_Q_morph _ (1#p)). + apply CRealLe_refl. + rewrite Qinv_plus_distr; reflexivity. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra Qminmax