proposition: Lemma cyclicS G H : H \subset G -> cyclic G -> cyclic H.
proof: Proof. move=> sHG /cyclicP[x defG]; apply/cyclicP. exists (x ^+ (#[x] %/ #|H|)); apply/congr_group/set1P. by rewrite -cycle_sub_group /order -defG ?cardSg // inE sHG eqxx. 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)