fact: Definition CRcauchy_sequence (xn : nat -> CR) : Set := forall p : positive, {n : nat | forall i j : nat, (n <= i)%nat -> (n <= j)%nat -> (' (1 # p) < CRabs (xn i - xn j))%CR -> False}.
imports: Coq.Reals.Abstract.ConstructiveReals CoRN.model.metric2.Qmetric CoRN.model.metric2.CRmetric CoRN.reals.fast.CRFieldOps CoRN.reals.fast.CRArith CoRN.reals.fast.CRabs CoRN.model.totalorder.QposMinMax Coq.Logic.ConstructiveEpsilon