proposition: Lemma esum_mkcondr [R : realType] [T : choiceType] (I J : set T) (a : T -> \bar R) : \esum_(i in I `&` J) a i = \esum_(i in I) if i \in J then a i else 0.
proof: Proof. rewrite esum_mkcond [RHS]esum_mkcond; apply: eq_esum=> i _. by rewrite in_setI; case: (i \in I) (i \in J) => [] []. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology sequences normedtype numfun