proposition: Theorem csum_zero_unit f j: sub j (domain f) -> (forall i, inc i ((domain f) -s j) -> (Vg f i) = \0c) -> csum f = csumb j (Vg f).
proof: Proof. move=> jdf acz; rewrite - csum_gr. congr cardinal; rewrite disjointU_E disjointU_E. set_extens x; move /setUf_P; aw; move => [y yd]; aw => h; apply/setUf_P; aw. case: (inc_or_not y j)=> yj; first by ex_tac; aw. have yc: (inc y ((domain f) -s j)) by apply /setC_P. move: h; rewrite (acz _ yc)=> /setX_P [_ /in_set0 [] _]. by exists y; aw; trivial;apply: jdf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)