proposition: Lemma cpow_sum a f: a ^c (csum f) = cprodb (domain f) (fun i => a ^c (Vg f i)).
proof: Proof. transitivity (a ^c (disjointU (Lg (domain f) (Vg f)))). by apply: cpow_pr => //; rewrite - (csum_gr) /csumb /csum; aw. rewrite -cprod_of_same {1}/cprodb /disjointU. set S:= disjointU_fam _; set f0:= Lg _ _. have pfa:partition_w_fam S (domain f0). by move: (partition_disjointU (Lg (domain f) (Vg f))); rewrite /f0; aw. rewrite (cprod_An pfa) /S /disjointU_fam ! Lgd;apply cprodb_exten. move=> x xdf; rewrite !LgV // /cprodb - cpowcr -(cardinal_indexed (Vg f x) x). rewrite cpowcr - cprod_of_same; congr cprod. apply: Lg_exten => t tw. rewrite LgV //. apply /setUb_P; rewrite /S /disjointU_fam; aw; ex_tac;rewrite !LgV//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)