proposition: Lemma dual_fsumeE (I : choiceType) (P : set I) (F : I -> \bar R) : (\sum_(i \in P) F i)%dE = (- (\sum_(i \in P) (- F i)))%E.
proof: Proof. rewrite finite_supportNe. 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 boolp classical_sets functions) mathcomp(fsbigop cardinality set_interval) reals signed topology constructive_ereal