proposition: Lemma CReal_cv_self' : forall (x : CReal) (n : Z), CReal_abs (x - inject_Q (seq x n)) <= inject_Q (2^n).
proof: Proof. intros x n [k kmaj]. unfold CReal_abs, CReal_abs_seq, CReal_abs_scale in kmaj. unfold CReal_minus, CReal_plus, CReal_plus_seq, CReal_abs_scale in kmaj. unfold CReal_opp, CReal_opp_seq, CReal_opp_scale in kmaj. unfold inject_Q in kmaj. do 4 rewrite CReal_red_seq in kmaj; rewrite Qred_correct in kmaj. apply (Qlt_not_le _ _ kmaj). clear kmaj. rewrite CReal_red_seq. apply (Qplus_le_l _ _ (2^n)%Q); ring_simplify. pose proof cauchy x (Z.max (k-1)%Z n) (k-1)%Z n ltac:(lia) ltac:(lia) as Hxbnd. apply Qlt_le_weak in Hxbnd. apply (Qle_trans _ _ _ Hxbnd); clear Hxbnd. apply Z.max_case. - rewrite <- Qplus_0_l; apply Qplus_le_compat. + apply Qpower_pos; lra. + rewrite Qpower_minus_pos. pose proof (Qpower_0_lt 2 k)%Q; lra. - rewrite <- Qplus_0_r; apply Qplus_le_compat. + lra. + pose proof (Qpower_0_lt 2 k)%Q; lra. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra