proposition: Lemma inject_Q_compare : forall (x : CReal) (p : Z), x <= inject_Q (seq x p + (2^p)).
proof: Proof. intros x p [n nmaj]. cbn in nmaj. assert(2^n>0)%Q by (apply Qpower_0_lt; lra). assert(2^p>0)%Q by (apply Qpower_0_lt; lra). pose proof x.(cauchy) as xcau. destruct (Z.min_dec p n); [ specialize (xcau n n p ltac:(lia) ltac:(lia)) | specialize (xcau p n p ltac:(lia) ltac:(lia)) ]. all: apply Qabs_Qlt_condition in xcau; lra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra