fact: Definition Cauchy_series (a : nat -> V) := forall eps : posreal, exists N : nat, forall n m : nat, (N <= n)%nat -> (N <= m)%nat -> norm (sum_n_m a n m) < eps.
imports: Coq(Reals Psatz ssreflect) Rcomplements Lim_seq Rbar Hierarchy