proposition: Lemma injm_cyclic G H (f : {morphism G >-> rT}) : 'injm f -> H \subset G -> cyclic (f @* H) = cyclic H.
proof: Proof. move=> injf sHG; apply/idP/idP; last exact: morphim_cyclic. by rewrite -{2}(morphim_invm injf sHG); apply: morphim_cyclic. 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)