proposition: Lemma cycle_subgroup_char a (H : {group gT}) : H \subset <[a]> -> H \char <[a]>.
proof: Proof. move=> sHa; apply: lone_subgroup_char => // J sJa isoJH. have dvHa: #|H| %| #[a] by apply: cardSg. have{dvHa} /setP Huniq := esym (cycle_sub_group dvHa). move: (Huniq H) (Huniq J); rewrite !inE /=. by rewrite sHa sJa (card_isog isoJH) eqxx => /eqP<- /eqP<-. 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)