proposition: Lemma CReal_cv_self : forall (x : CReal) (n : positive), CReal_abs (x - inject_Q (seq x (Z.neg n))) <= inject_Q (1#n).
proof: Proof. intros x n. apply CRealLt_asym. apply (CRealLt_RQ_from_single_dist _ _ (Z.neg n - 1)%Z). unfold CReal_abs, CReal_abs_seq, CReal_abs_scale. unfold CReal_minus, CReal_plus, CReal_plus_seq, CReal_abs_scale. unfold CReal_opp, CReal_opp_seq, CReal_opp_scale. unfold inject_Q. do 4 rewrite CReal_red_seq; rewrite Qred_correct. ring_simplify (Z.neg n - 1 - 1)%Z. pose proof cauchy x (Z.neg n) (Z.neg n - 2)%Z (Z.neg n) ltac:(lia) ltac:(lia) as Hxbnd. apply Qopp_lt_compat in Hxbnd. apply (Qplus_lt_r _ _ (1#n)) in Hxbnd. apply (Qlt_trans_swap_hyp _ _ _ Hxbnd); clear Hxbnd x. rewrite Qpower_minus_pos. apply (Qplus_lt_r _ _ (2 ^ Z.neg n)%Q); ring_simplify. pose proof Qpower_2powneg_le_inv n as Hpowinv. pose proof Qpower_0_lt 2 (Z.neg n) ltac:(lra) as Hpowpos. lra. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra