fact: Definition partial_sum {I : choiceType} {R : zmodType} (x : I -> R) (A : {fset I}) : R := \sum_(i : A) x (val i).
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(interval zmodp) mathcomp(boolp classical_sets) ereal reals Rstruct signed topology normedtype