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 * 2^(Z.min (-k-1) n) < seq y p - seq x p)%Q.
proof: Proof. intros x y n Hapart. pose proof CRealLt_aboveSig x y n Hapart. destruct (QarchimedeanExp2_Z (/ (seq y n - seq x n - (2 * 2 ^ n)))) as [k kmaj]. intros p Hp; specialize (H p Hp). pose proof Qpower_le_compat_l 2 (Z.min (- k -1) n) (- k-1) (Z.le_min_l _ _) ltac:(lra) as H1. rewrite Qpower_minus_pos in H1. apply (Qmult_le_compat_r _ _ 2) in H1. 2: lra. ring_simplify in H1. exact (Qle_lt_trans _ _ _ H1 H). Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra