proposition: Lemma fsumEFin (I : choiceType) A (F : I -> R) : finite_set A -> \sum_(i \in A) (F i)%:E = (\sum_(i \in A) F i)%:E.
proof: Proof. by move=> fs; rewrite fsbig_finite//= sumEFin -fsbig_finite. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal