proposition: Lemma CReal_from_cauchy_seq_bound : forall (xn : nat -> CReal) (xcau : Un_cauchy_mod xn) (i j : Z), (Qabs (CReal_from_cauchy_seq xn xcau i - CReal_from_cauchy_seq xn xcau j) <= 1)%Q.
proof: Proof. intros xn xcau i j. unfold CReal_from_cauchy_seq. destruct (xcau (4 * 2 ^ CReal_from_cauchy_cm i)%positive) as [i' imaj]. destruct (xcau (4 * 2 ^ CReal_from_cauchy_cm j)%positive) as [j' jmaj]. assert (CReal_abs (xn i' - xn j') <= inject_Q (1#4)) as Hxij. { 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; ring_simplify. apply Pos2Z_pos_is_pos. - 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; ring_simplify. apply Pos2Z_pos_is_pos. } clear imaj jmaj. unfold CReal_abs, CReal_abs_seq in Hxij. unfold CRealLe, CRealLt in Hxij. rewrite CReal_red_seq in Hxij. apply Qnot_lt_le; intros Hxij'; apply Hxij; clear Hxij. exists (-2)%Z. unfold inject_Q; rewrite CReal_red_seq. unfold CReal_minus, CReal_plus, CReal_plus_seq; rewrite CReal_red_seq, Qred_correct. unfold CReal_opp, CReal_opp_seq; rewrite CReal_red_seq. change (2 * 2 ^ (-2))%Q with (2#4)%Q. pose proof cauchy (xn i') (-3)%Z (-3)%Z (Z.neg (CReal_from_cauchy_cm i) - 2)%Z ltac:(lia) ltac:(unfold CReal_from_cauchy_cm; destruct i; lia) as Hxibnd. pose proof cauchy (xn j') (-3)%Z (-3)%Z (Z.neg (CReal_from_cauchy_cm j) - 2)%Z ltac:(lia) ltac:(unfold CReal_from_cauchy_cm; destruct j; lia) as Hxjbnd. apply (Qplus_lt_l _ _ (1 # 4)%Q); ring_simplify. setoid_replace (12#16)%Q with (3#4)%Q by ring. change (2^(-3))%Q with (1#8)%Q in Hxibnd, Hxjbnd. change (-2-1)%Z with (-3)%Z. apply Qabs_Qlt_condition in Hxibnd. apply Qabs_Qlt_condition in Hxjbnd. apply Qabs_Qgt_condition. apply Qabs_Qgt_condition in Hxij'. lra. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra Qminmax