proposition: Lemma perm_bigcprod (I : eqType) r1 r2 (A : I -> {set gT}) G x : \big[cprod/1]_(i <- r1) A i = G -> {in r1, forall i, x i \in A i} -> perm_eq r1 r2 -> \prod_(i <- r1) x i = \prod_(i <- r2) x i.
proof: Proof. elim: r1 r2 G => [|i r1 IHr] r2 G defG Ax eq_r12. by rewrite perm_sym in eq_r12; rewrite (perm_small_eq _ eq_r12) ?big_nil. have /rot_to[n r3 Dr2]: i \in r2 by rewrite -(perm_mem eq_r12) mem_head. transitivity (\prod_(j <- rot n r2) x j). rewrite Dr2 !big_cons in defG Ax *; have [[_ G1 _ defG1] _ _] := cprodP defG. rewrite (IHr r3 G1) //; first by case/allP/andP: Ax => _ /allP. by rewrite -(perm_cons i) -Dr2 perm_sym perm_rot perm_sym. rewrite -(cat_take_drop n r2) [in LHS]cat_take_drop in eq_r12 *. rewrite (perm_big _ eq_r12) !big_cat /= !(big_nth i) !big_mkord in defG *. have /cprodP[[G1 G2 defG1 defG2] _ /centsP-> //] := defG. rewrite defG2 -(bigcprodW defG2) mem_prodg // => k _; apply: Ax. by rewrite (perm_mem eq_r12) mem_cat orbC mem_nth. rewrite defG1 -(bigcprodW defG1) mem_prodg // => k _; apply: Ax. by rewrite (perm_mem eq_r12) mem_cat mem_nth. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(quotient action)