proposition: Lemma CRealLt_aboveSig : forall (x y : CReal) (n : Z), (2 * 2^n < seq y n - seq x n)%Q -> let (k, _) := QarchimedeanExp2_Z (/(seq y n - seq x n - (2 * 2 ^ n)%Q)) in forall p:Z, (p <= n)%Z -> (2^(-k) < seq y p - seq x p)%Q.
proof: Proof. intros x y n maj. destruct (QarchimedeanExp2_Z (/((seq y) n - (seq x) n - (2*2^n)%Q))) as [k kmaj]. intros p Hp. apply Qinv_lt_contravar in kmaj. 3: apply Qpower_0_lt; lra. 2: apply Qinv_lt_0_compat; lra. rewrite Qinv_involutive, <- Qpower_opp in kmaj; clear maj. pose proof ((cauchy x) n n p ltac:(lia) ltac:(lia)) as HCSx. pose proof ((cauchy y) n p n ltac:(lia) ltac:(lia)) as HCSy. rewrite Qabs_Qlt_condition in HCSx, HCSy. lra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra