proposition: Lemma csum_pr4 f: mutually_disjoint f -> cardinal (unionb f) = csumb (domain f) (fun a => cardinal (Vg f a)).
proof: Proof. move => pa; rewrite - csum_pr. apply: Eqc_disjointU => //; last exact (@disjointU_disjoint f). by rewrite /disjointU_fam; saw => i idx; rewrite LgV // Eq_indexed_c. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)