proposition: Lemma CRealLt_above : forall (x y : CReal), CRealLt x y -> { n : Z | forall p : Z, (p <= n)%Z -> (2 * 2 ^ n < seq y p - seq x p)%Q }.
proof: Proof. intros x y [n maj]. pose proof (CRealLt_aboveSig' x y n maj) as H. destruct (QarchimedeanExp2_Z (/ (seq y n - seq x n - (2 * 2 ^ n)))) as [k kmaj]. exists (Z.min (-k - 1) n)%Z; intros p Hp. apply H. lia. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra