proposition: Lemma sumeN I s (P : pred I) (f : I -> \bar R) : {in P &, forall i j, f i +? f j} -> \sum_(i <- s | P i) - f i = - \sum_(i <- s | P i) f i.
proof: Proof. elim: s => [|a b ih h]; first by rewrite !big_nil oppe0. rewrite !big_cons; case: ifPn => Pa; last by rewrite ih. by rewrite oppeD ?ih// adde_def_sum// => i Pi; rewrite h. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed