proposition: Lemma csum_pr1 f: cardinal (unionb f) <=c csumb (domain f) (fun a => cardinal (Vg f a)).
proof: Proof. rewrite -(csum_pr f);apply: surjective_cle. move: (disjointU_pr f) => /=; set g := common_ext _ _ _. by move => [sf tg srfj _]; exists g. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)