proposition: Lemma csum_zero_unit_bis f: (allf f (fun z => z = \0c)) <-> csum f = \0c.
proof: Proof. split. move => ha. have hc:(forall i, inc i (domain f -s emptyset) -> Vg f i = \0c). by move => i /setC_P [/ha ]. by rewrite (csum_zero_unit (sub0_set _) hc) csum_trivial0. move/card_nonempty; rewrite/disjointU /disjointU_fam => ue. move => i idf /=;case: (emptyset_dichot (Vg f i)) => // - [x xs]. empty_tac1 (J x i); apply/setUb_P; exists i; aw; trivial. by rewrite LgV//; apply: indexed_pi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)