proposition: Lemma csum_pr1_bis X f: cardinal (unionf X f) <=c csumb X (fun a => cardinal (f a)).
proof: Proof. rewrite setU_bf; move:(csum_pr1 (Lg X f));congr (_ <=c _). by aw; apply:csumb_exten => t tx; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)