fact: Definition QCauchySeq (xn : Z -> Q) : Prop := forall (k : Z) (p q : Z), Z.le p k -> Z.le q k -> Qabs (xn p - xn q) < 2 ^ k.
imports: QArith Qpower Qabs Qround Logic.ConstructiveEpsilon Lia Lqa QExtra ConstructiveExtra