proposition: Lemma gen_prodgP A x : reflect (exists n, exists2 c, forall i : 'I_n, c i \in A & x = \prod_i c i) (x \in <<A>>).
proof: Proof. apply: (iffP idP) => [|[n [c Ac ->]]]; last first. by apply: group_prod => i _; rewrite mem_gen ?Ac. have [n ->] := gen_expgs A; rewrite /expgn Monoid.iteropE /=. rewrite -[n]card_ord -big_const => /prodsgP[/= c Ac def_x]. have{Ac def_x} ->: x = \prod_(i | c i \in A) c i. rewrite big_mkcond {x}def_x; apply: eq_bigr => i _. by case/setU1P: (Ac i isT) => -> //; rewrite if_same. have [e <- [_ /= mem_e] _] := big_enumP [preim c of A]. pose t := in_tuple e; rewrite -[e]/(val t) big_tuple. by exists (size e), (c \o tnth t) => // i; rewrite -mem_e mem_tnth. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype div path tuple bigop prime finset)