proposition: Theorem Thompson_transitivity p q A : A \in 'SCN_3[p] -> q \in p^' -> [transitive 'O_p^'('C(A)), on |/|*(A; q) | 'JG].
proof: Proof. case/bigcupP=> P; rewrite 2!inE => sylP /andP[SCN_A mA3]. have [defZ def_pi']: 'Z(A) = A /\ \pi(A)^' =i p^'. rewrite inE -andbA in SCN_A; case/and3P: SCN_A => sAP _ /eqP defCA. case: (eqsVneq A 1) mA3 => /= [-> | ntA _]. rewrite /rank big1_seq // => p1 _; rewrite /p_rank big1 // => E. by rewrite inE; case/andP; move/trivgP->; rewrite cards1 logn1. have [p_pr _ [k ->]] := pgroup_pdiv (pgroupS sAP (pHall_pgroup sylP)) ntA. split=> [|p1]; last by rewrite !inE primesX // primes_prime ?inE. by apply/eqP; rewrite eqEsubset subsetIl subsetI subxx -{1}defCA subsetIr. rewrite -(eq_pcore _ def_pi') -def_pi' => pi'q. apply: normed_constrained_rank3_trans; rewrite ?defZ //. by apply: SCN_normed_constrained sylP _; rewrite inE SCN_A ltnW. 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)