proposition: Theorem normed_constrained_rank2_trans : q %| #|'C(A)| -> 'r('Z(A)) >= 2 -> [transitive K, on |/|*(A; q) | 'JG].
proof: Proof. move=> qC /rank_geP[B /nElemP[p /setIdP[/setIdP[/subsetIP[sBA cAB] abelB] oB]]]. have [_ cBB _] := and3P abelB. have{abelB oB} ncycB: ~~ cyclic B by rewrite (abelem_cyclic abelB) (eqP oB). have [R0 sylR0] := Sylow_exists q 'C(A); have [cAR0 qR0 _] := and3P sylR0. have nR0A: A \subset 'N(R0) by rewrite cents_norm // centsC. have{nR0A} [R maxR sR0R] := max_normed_exists qR0 nR0A. apply/imsetP; exists R => //; apply/setP=> Q. apply/idP/imsetP=> [maxQ|[k Kk] ->]; last by rewrite actsKmax. have [qR nRA]:= mem_max_normed maxR; have [qQ nQA]:= mem_max_normed maxQ. have [R1 | ntR] := eqVneq R 1%G. rewrite trivg_max_norm -R1 // in maxQ. by exists 1; rewrite ?group1 ?act1 ?(set1P maxQ). have ntQ: Q != 1%G. by apply: contra ntR => Q1; rewrite trivg_max_norm -(eqP Q1) // inE in maxR *. have ntRC: 'C_R(A) != 1. have sR0CR: R0 \subset 'C_R(A) by rewrite subsetI sR0R. suffices: R0 :!=: 1 by apply: subG1_contra. move: ntR; rewrite -!cardG_gt1 -(part_pnat_id qR) (card_Hall sylR0). by rewrite !p_part_gt1 !mem_primes !cardG_gt0 qC => /and3P[->]. have: [exists (z | 'C_Q[z] != 1), z \in B^#]. apply: contraR ntQ => trQ; have:= subset_trans sBA nQA. rewrite -[_ == _]subG1=> /coprime_abelian_gen_cent1 <- //; last first. by rewrite coprime_sym (coprimeSg sBA) ?coprime_pi' /pgroup ?(pi_pnat qQ). rewrite gen_subG; apply/bigcupsP=> z Cz; rewrite subG1. by apply: contraR trQ => ntCz; apply/existsP; exists z; rewrite ntCz. case/existsP=> z; rewrite 2!inE => /and3P[ntzQ ntz Bz]. have prCz: 'C[z] \proper G by rewrite -cent_cycle mFT_cent_proper ?cycle_eq1. have sACz: A \subset 'C[z] by rewrite sub_cent1 (subsetP cAB). have [|//|k Kk defQ2]:= normed_constrained_meet_trans sACz prCz maxR maxQ. apply: subG1_contra ntRC; rewrite setIS //=. by rewrite -cent_cycle centS // cycle_subG (subsetP sBA). by exists k => //; apply: val_inj. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div choice fintype bigop) mathcomp(finset prime fingroup morphism automorphism action quotient) mathcomp(gfunctor cyclic pgroup center commutator gseries nilpotent) mathcomp(sylow abelian maximal hall) odd_order(BGsection1 BGsection6)