proposition: Lemma CReal_scale_sep0_limit : forall (x : CReal) (n : Z), (2 * (2^n)%Q < seq x n)%Q -> (n <= scale x - 2)%Z.
proof: Proof. intros x n Hnx. pose proof bound x n as Hxbnd. apply Qabs_Qlt_condition in Hxbnd. destruct Hxbnd as [_ Hxbnd]. apply (Qlt_trans _ _ _ Hnx) in Hxbnd. replace n with ((n+1)-1)%Z in Hxbnd by lia. rewrite Qpower_minus_pos in Hxbnd by lra. simplify_Qlt_in Hxbnd. apply (Qpower_lt_compat_l_inv) in Hxbnd. - lia. - lra. Qed.
imports: QArith Qabs Qround Qpower Logic.ConstructiveEpsilon ConstructiveCauchyReals Lia Lqa QExtra