proposition: Theorem csum_An f g: partition_w_fam g (domain f) -> csum f = csumb (domain g) (fun l => csumb (Vg g l) (Vg f)).
proof: Proof. move=> pfg; rewrite/csumb/csum; set h := fun l:Set => _. rewrite/disjointU/disjointU_fam Lgd. set g0 := fun i:Set => _. transitivity (cardinal (unionb (Lg (domain g) (fun l => unionf (Vg g l) g0)))). f_equal;rewrite /unionb; aw;rewrite - (proj33 pfg) setUf_A. apply: setUf_exten; move => t tdf; rewrite LgV//. apply: setUf_exten; move=> i idg; rewrite LgV//; union_tac. apply: Eqc_disjointU;fprops; aw; last first. - by apply: mutually_disjoint_prop3. - apply: mutually_disjoint_prop2; rewrite /g0=> u v y udg vdg; aw. move /setUf_P => [u' u'Vg /setX_P [py Py /set1_P Qy]]. move /setUf_P => [v' v'Vg /setX_P [py' Py' /set1_P Qy']]. case :(proj32 pfg _ _ udg vdg) =>// di. rewrite -Qy' Qy in v'Vg; case: (nondisjoint u'Vg v'Vg di). split; aww => i idg; rewrite !LgV//. rewrite setU_bf /h /disjointU/disjointU_fam /g0; aw; trivial. apply: Eqc_disjointU; try apply:mutually_disjoint_prop3. by split; aww; move=> j jVg; rewrite !LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)