proposition: Lemma CRealLe_not_lt : forall x y : CReal, (forall n : Z, (seq x n - seq y n <= 2 * 2 ^ n)%Q) <-> x <= y.
proof: Proof. intros. split. - intros H H0. destruct H0 as [n H0]; specialize (H n); lra. - intros H n. destruct (Qlt_le_dec (2 * 2 ^ n) (seq x n - seq y n)). + exfalso. apply H. exists n. assumption. + assumption. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra