fact: Definition sum (I : choiceType) {K : numDomainType} {R : normedModType K} (x : I -> R) : R := lim (partial_sum x @ totally).
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(interval zmodp) mathcomp(boolp classical_sets) ereal reals Rstruct signed topology normedtype