proposition: Lemma DRealAbstrFalse : forall (x : CReal) (q : Q) (n : nat), proj1_sig (DRealAbstr x) q = false -> (seq x (- Z.of_nat n) <= q + 2 ^ (- Z.of_nat n))%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. - apply H'. Qed.
imports: Coq.Logic.Eqdep_dec Coq.Logic.FunctionalExtensionality Coq.Logic.HLevels QArith Qabs ConstructiveCauchyReals ConstructiveRcomplete Lia Lqa Qpower QExtra