proposition: Lemma CRealLt_QR_to_single_dist : forall (q : Q) (x : CReal) (n : Z), inject_Q q < x -> (-(2^n) <= seq x n - q)%Q.
proof: Proof. intros q x n Hqltx. destruct (Qlt_le_dec (seq x n - q) (-(2^n)) ) as [Hdec|Hdec]. - exfalso. pose proof CRealLt_RQ_from_single_dist x q n ltac:(lra) as contra. apply CRealLt_asym in contra. apply contra, Hqltx. - apply Hdec. Qed.
imports: QArith_base Qabs ConstructiveReals ConstructiveCauchyRealsMult Logic.ConstructiveEpsilon ConstructiveCauchyAbs Lia Lqa Qpower QExtra PosExtra ConstructiveExtra Qminmax