proposition: Lemma injm_generator G H (f : {morphism G >-> rT}) x : 'injm f -> x \in G -> H \subset G -> generator (f @* H) (f x) = generator H x.
proof: Proof. move=> injf Gx sHG; apply/idP/idP; last exact: morph_generator. rewrite -{2}(morphim_invm injf sHG) -{2}(invmE injf Gx). by apply: morph_generator; apply: mem_morphim. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm automorphism quotient gproduct ssralg) mathcomp(finalg zmodp poly)