proposition: Lemma dual_sumeE I (r : seq I) (P : pred I) (F : I -> \bar^d R) : (\sum_(i <- r | P i) F i)%dE = - (\sum_(i <- r | P i) (- F i)%E)%E.
proof: Proof. apply: (big_ind2 (fun x y => x = - y)%E) => [|_ x _ y -> ->|i _]. - by rewrite oppe0. - by rewrite dual_addeE !oppeK. - by rewrite oppeK. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed