proposition: Lemma sumEFin I s P (F : I -> R) : \sum_(i <- s | P i) (F i)%:E = (\sum_(i <- s | P i) F i)%:E.
proof: Proof. by rewrite (big_morph _ EFinD erefl). Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed