proposition: Lemma dsumEFin I r P (F : I -> R) : \sum_(i <- r | P i) (F i)%:E = (\sum_(i <- r | P i) F i)%R%:E.
proof: Proof. by rewrite dual_sumeE fin_num_sumeN// oppeK sumEFin. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed