proposition: Lemma csum_pr4_bis X f: (forall i j, inc i X -> inc j X -> i = j \/ disjoint (f i) (f j)) -> cardinal (unionf X f) = csumb X (fun a => cardinal (f a)).
proof: Proof. move => mdx1. have mdx: mutually_disjoint (Lg X f). by hnf; aw => i j iX jX; rewrite !LgV //; apply:mdx1. by rewrite setU_bf (csum_pr4 mdx); aw; apply:csumb_exten => t tx; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)