proposition: Lemma extremal_generators_facts gT (G : {group gT}) p n x y : prime p -> extremal_generators G p n (x, y) -> [/\ p.-group G, maximal <[x]> G, <[x]> <| G, <[x]> * <[y]> = G & <[y]> \subset 'N(<[x]>)].
proof: Proof. move=> p_pr [oG Gx ox] /setDP[Gy notXy]. have pG: p.-group G by rewrite /pgroup oG pnatX pnat_id. have maxX: maximal <[x]> G. rewrite p_index_maximal -?divgS ?cycle_subG // -orderE oG ox. case: (n) oG => [|n' _]; last by rewrite -expnB ?subSnn ?leqnSn ?prime_gt0. move/eqP; rewrite -trivg_card1; case/trivgPn. by exists y; rewrite // (group1_contra notXy). have nsXG := p_maximal_normal pG maxX; split=> //. by apply: mulg_normal_maximal; rewrite ?cycle_subG. by rewrite cycle_subG (subsetP (normal_norm nsXG)). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism presentation) mathcomp(quotient action commutator gproduct gfunctor) mathcomp(ssralg countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule matrix maximal)