proposition: Lemma DRealAbstrFalse'' : forall (x : CReal) (q : Q) (n : Z), proj1_sig (DRealAbstr x) q = false -> (seq x n <= q + 2^n + 1)%Q.
proof: Proof. intros x q n H. unfold DRealAbstr, proj1_sig in H. match type of H with context [ if ?a then _ else _ ] => destruct a as [H'|H']end. - discriminate. - destruct (Z_le_gt_dec n 0) as [Hdec|Hdec]. + specialize (H' (Z.to_nat (-n) )). rewrite (Z2Nat.id (-n)%Z ltac:(lia)), Z.opp_involutive in H'. pose proof Qpower_0_lt 2 n; lra. + specialize (H' (Z.to_nat (0) )). cbn in H'. pose proof cauchy x n%Z 0%Z n ltac:(lia) ltac:(lia) as Hxbnd. apply Qabs_Qlt_condition in Hxbnd. lra. Qed.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra