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