proposition: Lemma CReal_of_DReal_seq_bound : forall (x : DReal) (i j : Z), (Qabs (CReal_of_DReal_seq x i - CReal_of_DReal_seq x j) <= 1)%Q.
proof: Proof. intros x i j. pose proof CReal_of_DReal_cauchy x 0%Z as Hcau. apply Qlt_le_weak; change (2^0)%Q with 1%Q in Hcau. destruct (Z_gt_le_dec i 0) as [Hi|Hi]; destruct (Z_gt_le_dec j 0) as [Hj|Hj]. all: try rewrite (CReal_of_DReal_seq_max_prec_1 x i) by lia; try rewrite (CReal_of_DReal_seq_max_prec_1 x j) by lia; apply Hcau; lia. Qed.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra