proposition: Theorem normed_constrained_rank3_trans : 'r('Z(A)) >= 3 -> [transitive K, on |/|*(A; q) | 'JG].
proof: Proof. case/rank_geP=> B /nElemP[p]; rewrite !inE subsetI -2!andbA. case/and4P=> sBA cAB abelB mB3; have [_ cBB _] := and3P abelB. have q'B: forall Q, q.-group Q -> coprime #|Q| #|B|. move=> Q qQ; rewrite coprime_sym (coprimeSg sBA) ?coprime_pi' //. exact: pi_pnat qQ _. have [Q1 maxQ1 _] := max_normed_exists (pgroup1 _ q) (norms1 A). apply/imsetP; exists Q1 => //; apply/setP=> Q2. apply/idP/imsetP=> [maxQ2|[k Kk] ->]; last by rewrite actsKmax. have [qQ1 nQ1A]:= mem_max_normed maxQ1; have [qQ2 nQ2A]:= mem_max_normed maxQ2. case: (eqVneq Q1 1%G) => [trQ1 | ntQ1]. exists 1; rewrite ?group1 // act1; apply/eqP. by rewrite trivg_max_norm -trQ1 // inE in maxQ2. case: (eqVneq Q2 1%G) => [trQ2 | ntQ2]. by case/negP: ntQ1; rewrite trivg_max_norm -trQ2 // inE in maxQ1 *. have: [exists (C : grT | 'C_Q1(C) != 1), cyclic (B / C) && (C <| B)]. apply: contraR ntQ1 => trQ1; have: B \subset 'N(Q1) := subset_trans sBA nQ1A. rewrite -val_eqE -subG1 /=; move/coprime_abelian_gen_cent <-; rewrite ?q'B //. rewrite gen_subG; apply/bigcupsP=> C cocyC; rewrite subG1. by apply: contraR trQ1 => ntCC; apply/existsP; exists C; rewrite ntCC. case/existsP=> C /and3P[ntCQ1 cycBC nsCB]; have [sCB nCB]:= andP nsCB. have{mB3} ncycC: ~~ cyclic C. rewrite (abelem_cyclic (quotient_abelem _ abelB)) ?card_quotient // in cycBC. rewrite -divgS // logn_div ?cardSg // leq_subLR addn1 (eqP mB3) in cycBC. by rewrite (abelem_cyclic (abelemS sCB abelB)) -ltnNge. have: [exists (z | 'C_Q2[z] != 1), z \in C^#]. apply: contraR ntQ2 => trQ2; have:= subset_trans sCB (subset_trans sBA nQ2A). rewrite -[_ == _]subG1 /=. move/coprime_abelian_gen_cent1 <-; rewrite ?(abelianS sCB) //; last first. by rewrite (coprimegS sCB) ?q'B. rewrite gen_subG; apply/bigcupsP=> z Cz. by apply: contraR trQ2 => ntCz; apply/existsP; exists z; rewrite -subG1 ntCz. case/existsP=> z; rewrite !inE => /and3P[ntzQ2 ntz Cz]. 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) ?(subsetP sCB). have [|//|k Kk defQ2]:= normed_constrained_meet_trans sACz prCz maxQ1 maxQ2. by apply: subG1_contra ntCQ1; rewrite setIS //= -cent_cycle centS ?cycle_subG. 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)