proposition: Lemma CReal_abs_appart_zero : forall (x : CReal) (n : Z), (2*2^n < Qabs (seq x n))%Q -> 0 # x.
proof: Proof. intros x n Hapart. unfold CReal_appart. destruct (Qlt_le_dec 0 (seq x n)). - left; exists n; cbn. rewrite Qabs_pos in Hapart; lra. - right; exists n; cbn. rewrite Qabs_neg in Hapart; lra. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra