proposition: Theorem cprodDn f: cprodb (domain f) (fun l => csum (Vg f l)) = csumb (productf (domain f) (fun l => (domain (Vg f l)))) (fun g => (cprodb (domain f) (fun l => Vg (Vg f l) (Vg g l)))).
proof: Proof. transitivity (cprodb (domain f) (fun l => disjointU (Vg f l))). by apply: Eqc_setXb;split; aww => i idf; rewrite /csum !LgV //; aw. set (g:= Lg (domain f) (fun l => disjointU_fam (Vg f l))). transitivity(cprodb (domain g) (fun l => unionb (Vg g l))). rewrite/cprodb /cprod /g; f_equal; f_equal. aw; apply: Lg_exten; move=> x xdg; rewrite LgV//. rewrite/cprodb/cprod -/(productf _ _) distrib_prod_union //. have dg: domain g = domain f by rewrite /g; aw. set ld:= productf _ _. have lde: ld = productf (domain f) (fun l => domain (Vg f l)). rewrite /ld/productf dg; apply: f_equal; apply: Lg_exten. by move=> x xdg; rewrite /g LgV // Lgd. rewrite setU_bf - lde. apply: Eqc_disjointU;last by fprops. saw; first by rewrite/ disjointU_fam; aw. move=> i ip; rewrite !LgV //; aw; trivial. set h := (productb (Lg (domain f) (fun l => Vg (Vg f l) (Vg i l)))). apply: Eqc_setXb; split => //; aww. move=> k kdg; rewrite /g /disjointU_fam -dg; aw; rewrite !LgV //; aw; trivial. move: ip; rewrite lde; move/setXf_P => [_ dif]; apply; ue. have myel: forall i j y, inc i ld -> inc y (productf (domain f) (fun l => Vg (Vg g l) (Vg i l))) -> inc j (domain f) -> Q (Vg y j) = Vg i j. rewrite /g/ disjointU_fam lde. move=>k j y; aw=> /setXf_P [fgk dk kp1] /setXf_P [fgy dy yp1] jdf. move: (kp1 _ jdf)=> iVjk. by move: (yp1 _ jdf); rewrite !LgV //; move /setX_P => [_ _ /set1_P]. apply: mutually_disjoint_prop; aw. move=>i j y ild jld; rewrite dg !LgV // => xp yp. apply: (setXf_exten ild jld) => k kdf /=; rewrite dg in kdf. by rewrite - (myel _ _ _ ild xp kdf) - (myel _ _ _ jld yp kdf). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)