proposition: Lemma csum_trivial f: domain f = emptyset -> csum f = \0c.
proof: Proof. move=> dge; rewrite/csum /disjointU /disjointU_fam dge /Lg funI_set0. by rewrite setUb_0 cardinal_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)