fact: Definition espc mu f A := sum (fun x => f x * prc mu (pred1 x) A).
imports: mathcomp(all_ssreflect all_algebra) mathcomp.classical(boolp classical_sets mathcomp_extra) xfinmap ereal reals discrete topology realseq realsum