proposition: Lemma CRealLe_0R_to_single_dist : forall (x : CReal) (n : Z), 0 <= x -> (-(2^n) <= seq x n)%Q.
proof: Proof. intros x n Hxnonneg. destruct (Qlt_le_dec (seq x n) (-(2^n))) as [Hdec|Hdec]. - exfalso; apply Hxnonneg. apply (CRealLt_RQ_from_single_dist x 0 n); lra. - exact Hdec. Qed.
imports: QArith Qabs Qpower ConstructiveCauchyReals ConstructiveCauchyRealsMult Lia Lqa QExtra