proposition: Lemma pi_Aut_rank2_pgroup gT p q (R : {group gT}) : p.-group R -> odd #|R| -> 'r(R) <= 2 -> q \in \pi(Aut R) -> q != p -> [/\ q %| (p ^ 2).-1, q < p & q %| p.+1./2 \/ q %| p.-1./2].
proof: Proof. move=> pR oddR rR q_Ar p'q; rewrite /= in q_Ar. have [R1 | ntR] := eqsVneq R 1; first by rewrite R1 Aut1 cards1 in q_Ar. have{ntR} [p_pr p_dv_R _] := pgroup_pdiv pR ntR. have{oddR p_dv_R} [p_odd p_gt1] := (dvdn_odd p_dv_R oddR, prime_gt1 p_pr). have{q_Ar} [q_pr q_dv_Ar]: prime q /\ q %| #|Aut R|. by move: q_Ar; rewrite mem_primes; case/and3P. suffices q_dv_p2: q %| (p ^ 2).-1. have q_dv_p1: q %| p.+1./2 \/ q %| p.-1./2. apply/orP; have:= q_dv_p2; rewrite -subn1 (subn_sqr p 1). rewrite -[p]odd_double_half p_odd /= !doubleK addKn addn1 -doubleS -!mul2n. rewrite mulnC !Euclid_dvdM // dvdn_prime2 // -orbA; case: eqP => // -> _. by rewrite -Euclid_dvdM // /dvdn modn2 mulnC oddM andbN. have p_gt2: p > 2 by rewrite ltn_neqAle; case: eqP p_odd => // <-. have p1_ltp: p.+1./2 < p. by rewrite -divn2 ltn_divLR // muln2 -addnn -addn2 leq_add2l. split=> //; apply: leq_ltn_trans p1_ltp. move/orP: q_dv_p1; rewrite -(subnKC p_gt2) leqNgt. by apply: contraL => lt_p1q; rewrite negb_or !gtnNdvd // ltnW. wlog{q_dv_Ar} [a oa nRa]: gT R pR rR / {a | #[a] = q & a \in 'N(R) :\: 'C(R)}. have [a Ar_a oa] := Cauchy q_pr q_dv_Ar. rewrite -(injm_rank (injm_sdpair1 [Aut R])) // in rR. move=> IH; apply: IH rR _; rewrite ?morphim_pgroup ?morphim_odd //. exists (sdpair2 [Aut R] a); rewrite ?(order_injm (injm_sdpair2 _)) //. rewrite inE (subsetP (im_sdpair_norm _)) ?mem_morphim //= andbT. apply: contraL (prime_gt1 q_pr) => cRa; rewrite -oa order_gt1 negbK. apply/eqP; apply: (eq_Aut Ar_a (group1 _)) => x Rx. by rewrite perm1 [a x](@astab_act _ _ _ [Aut R] R) ?astabEsd ?mem_morphpre. move: {2}_.+1 (ltnSn #|R|) => n. elim: n => // n IHn in gT a R pR rR nRa oa *; rewrite ltnS => leRn. case recR: [exists (S : {group gT} | S \proper R), a \in 'N(S) :\: 'C(S)]. have [S ltSR nSa] := exists_inP recR; rewrite properEcard in ltSR. have{ltSR} [sSR ltSR] := andP ltSR; have rS := leq_trans (rankS sSR) rR. by apply: IHn nSa oa _; rewrite ?(pgroupS sSR) ?(leq_trans ltSR). do [rewrite inE -!cycle_subG orderE; set A := <[a]>] in nRa oa. have{nRa oa} [[not_cRA nRA] oA] := (andP nRa, oa). have coRA : coprime #|R| #|A| by rewrite oA (pnat_coprime pR) ?pnatE. have{recR} IH: forall S, gval S \proper R -> A \subset 'N(S) -> A \subset 'C(S). move=> S ltSR; rewrite !cycle_subG => nSa; apply: contraFT recR => not_cSa. by apply/exists_inP; exists S; rewrite // inE not_cSa nSa. have defR1: 'Ohm_1(R) = R. apply: contraNeq not_cRA; rewrite eqEproper Ohm_sub negbK => ltR1R. rewrite (coprime_odd_faithful_Ohm1 pR) ?IH ?(odd_pgroup_odd p_odd) //. exact: gFnorm_trans. have defRA: [~: R, A] = R. apply: contraNeq not_cRA; rewrite eqEproper commg_subl nRA negbK => ltRAR. rewrite centsC; apply/setIidPl. rewrite -{2}(coprime_cent_prod nRA) ?(pgroup_sol pR) //. by rewrite mulSGid // subsetI commg_subl nRA centsC IH ?commg_normr. have [cRR | not_cRR] := boolP (abelian R). rewrite -subn1 (subn_sqr p 1) Euclid_dvdM //. have abelR: p.-abelem R by rewrite -defR1 Ohm1_abelem. have ntR: R :!=: 1 by apply: contraNneq not_cRA => ->; apply: cents1. pose rAR := reprGLm (abelem_repr abelR ntR nRA). have:= cardSg (subsetT (rAR @* A)); rewrite card_GL ?card_Fp //. rewrite card_injm ?ker_reprGLm ?rker_abelem ?prime_TIg ?oA // unlock. rewrite Gauss_dvdr; last by rewrite coprimeXr ?prime_coprime ?dvdn_prime2. move: rR; rewrite -ltnS -[_ < _](mem_iota 0) !inE eqn0Ngt rank_gt0 ntR. rewrite (dim_abelemE abelR ntR) (rank_abelem abelR). do [case/pred2P=> ->; rewrite /= muln1] => [-> // | ]. by rewrite (subn_sqr p 1) mulnA !Euclid_dvdM ?orbb. have [[defPhi defR'] _]: special R /\ 'C_R(A) = 'Z(R). apply: (abelian_charsimple_special pR) => //. apply/bigcupsP=> S /andP[charS cSS]. rewrite centsC IH ?(char_norm_trans charS) // properEneq char_sub // andbT. by apply: contraNneq not_cRR => <-. have ntZ: 'Z(R) != 1 by rewrite -defR' (sameP eqP derG1P). have ltRbR: #|R / 'Z(R)| < #|R| by rewrite ltn_quotient ?center_sub. have pRb: p.-group (R / 'Z(R)) by apply: quotient_pgroup. have nAZ: A \subset 'N('Z(R)) by apply: gFnorm_trans. have defAb: A / 'Z(R) = <[coset _ a]> by rewrite quotient_cycle -?cycle_subG. have oab: #[coset 'Z(R) a] = q. rewrite orderE -defAb -(card_isog (quotient_isog _ _)) //. by rewrite coprime_TIg ?(coprimeSg (center_sub R)). have rRb: 'r(R / 'Z(R)) <= 2. rewrite (rank_pgroup pRb) (leq_trans (p_rank_le_logn _ _)) // -ltnS. apply: leq_trans (rank2_exponent_p_p3group pR rR _). by rewrite -(ltn_exp2l _ _ p_gt1) -!card_pgroup. by rewrite -defR1 (exponent_Ohm1_class2 p_odd) // nil_class2 defR'. apply: IHn oab (leq_trans ltRbR leRn) => //. rewrite inE -!cycle_subG -defAb quotient_norms ?andbT //. apply: contra not_cRA => cRAb; rewrite (coprime_cent_Phi pR coRA) // defPhi. by rewrite commGC -quotient_cents2 ?gFnorm. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finfun bigop ssralg finset prime binomial) mathcomp(fingroup morphism automorphism perm quotient action gproduct) mathcomp(gfunctor commutator zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)