proposition: Lemma morphim_cyclic rT G H (f : {morphism G >-> rT}) : cyclic H -> cyclic (f @* H).
proof: Proof. move=> cycH; wlog sHG: H cycH / H \subset G. by rewrite -morphimIdom; apply; rewrite (cyclicS _ cycH, subsetIl) ?subsetIr. case/cyclicP: cycH sHG => x ->; rewrite gen_subG sub1set => Gx. by apply/cyclicP; exists (f x); rewrite morphim_cycle. 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)