proposition: Lemma cycle_sub_group (a : gT) m : m %| #[a] -> [set H : {group gT} | H \subset <[a]> & #|H| == m] = [set <[a ^+ (#[a] %/ m)]>%G].
proof: Proof. move=> m_dv_a; have m_gt0: 0 < m by apply: dvdn_gt0 m_dv_a. have oam: #|<[a ^+ (#[a] %/ m)]>| = m. apply/eqP; rewrite [#|_|]orderXgcd -(divnMr m_gt0) muln_gcdl divnK //. by rewrite gcdnC gcdnMr mulKn. apply/eqP; rewrite eqEsubset sub1set inE /= cycleX oam eqxx !andbT. apply/subsetP=> X; rewrite in_set1 inE -val_eqE /= eqEcard oam. case/andP=> sXa /eqP oX; rewrite oX leqnn andbT. apply/subsetP=> x Xx; case/cycleP: (subsetP sXa _ Xx) => k def_x. have: (x ^+ m == 1)%g by rewrite -oX -order_dvdn cardSg // gen_subG sub1set. rewrite {x Xx}def_x -expgM -order_dvdn -[#[a]](Lagrange sXa) -oX mulnC. rewrite dvdn_pmul2r // mulnK // => /dvdnP[i ->]. by rewrite mulnC expgM groupX // cycle_id. 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)