proposition: Lemma finite_card_sum (A : set T) : finite_set A -> \esum_(i in A) 1 = (#|` fset_set A|%:R)%:E :> \bar R.
proof: Proof. move=> finA; rewrite esum_fset// (eq_fsbigr (cst 1))//. by rewrite card_fset_sum1// natr_sum -sumEFin fsbig_finite. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)