proposition: Fact csum_prod_assoc_aux I J (f: fterm2): csumb I (fun i => csumb J (fun j => f i j)) = csumb J (fun j => csumb I (fun i => f i j)) /\ cprodb I (fun i => cprodb J (fun j => f i j)) = cprodb J (fun j => cprodb I (fun i => f i j)).
proof: Proof. pose h := Lg (I \times J) (fun z => f (P z) (Q z)). pose g1 := Lg I (fun i => indexedr i J). pose g2 := Lg J (fun j => indexed I j). have par2: partition_w_fam g2 (domain h). rewrite /g2 /h; split. - fprops. - apply: mutually_disjoint_prop3. - rewrite - setU_bf; aw;set_extens t. move=>/setUf_P [j jJ /indexed_P [pa pb pc]]. apply/setX_P; split => //; ue. by move/setX_P => [qa qb qc]; apply/setUf_P; ex_tac; apply/indexed_P. have par1: partition_w_fam g1 (domain h). rewrite /g1 /h; split. - fprops. - apply: mutually_disjoint_prop2 => u v y _ _. by move=> /setX_P [_ /set1_P <- _] /setX_P [_ /set1_P <- _]. - rewrite - setU_bf; aw; set_extens t. move=>/setUf_P [j jJ /indexedrP [pa pb pc]]. apply/setX_P; split => //; ue. by move/setX_P => [qa qb qc]; apply/setUf_P; ex_tac; apply/indexedrP. have qa i: inc i I -> quasi_bij Q (indexedr i J) J. move => iI; split. - by move => x /setX_P []. - move => x y /indexedrP [pa pb pc] /indexedrP [pa' pb' pc'] rq. apply: pair_exten => //; ue. - move => y yJ; exists (Pair.J i y); aw; last trivial. by apply/indexedrP; split; aww. have qb j: inc j J -> quasi_bij P (indexed I j) I. move => iI; split. - by move => x /setX_P []. - move => x y /indexed_P [pa pb pc] /indexed_P [pa' pb' pc'] rq. apply: pair_exten => //; ue. - move => y yJ; exists (Pair.J y j); aw; last trivial. by apply/indexed_P; split;aww. split. move: (csum_An par2); rewrite (csum_An par1) /g1/g2; aw. set A := csumb _ _; set B :=csumb _ _;set C := csumb _ _; set D:= csumb _ _. have ->: A = C. apply csumb_exten => i iI; rewrite LgV// (csum_Cn2 _ (qa _ iI)). apply: csumb_exten => j /indexedrP [sa sb sc]; rewrite/h LgV //; first ue. apply/setX_P; split => //; ue. have -> //: B = D. apply csumb_exten => i iI; rewrite LgV // (csum_Cn2 _ (qb _ iI)). apply: csumb_exten => j /indexed_P [sa sb sc]; rewrite/h LgV//; first ue. apply/setX_P; split => //; ue. move: (cprod_An par2); rewrite (cprod_An par1) /g1/g2; aw. set A := cprodb _ _; set B :=cprodb _ _;set C := cprodb _ _; set D:= cprodb _ _. have ->: A = C. apply cprodb_exten => i iI; rewrite LgV// (cprod_Cn2 _ (qa _ iI)). apply: cprodb_exten => j /indexedrP [sa sb sc]; rewrite/h LgV//; first ue. apply/setX_P; split => //; ue. have -> //: B = D. apply cprodb_exten => i iI;rewrite LgV// (cprod_Cn2 _ (qb _ iI)). apply: cprodb_exten => j /indexed_P [sa sb sc]; rewrite/h LgV//; first ue. apply/setX_P; split => //; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)