proposition: Lemma CRealEq_diff : forall (x y : CReal), CRealEq x y <-> forall n:Z, ((Qabs (seq x n - seq y n)) <= (2 * 2 ^ n))%Q.
proof: Proof. intros x y; split. - intros H n; destruct H as [Hyx Hxy]. pose proof (CRealLe_not_lt x y) as [_ Hxy']. specialize (Hxy' Hxy n). pose proof (CRealLe_not_lt y x) as [_ Hyx']. specialize (Hyx' Hyx n). apply Qabs_Qle_condition; lra. - intros H; split; apply CRealLe_not_lt; intro n; specialize (H n); apply Qabs_Qle_condition in H; lra. Qed.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra