proposition: Lemma primeTIhyp_quotient (M : {group gT}) : (W2 / M != 1)%g -> M \subset K -> M <| L -> {defWbar : (W1 / M) \x (W2 / M) = W / M & primeTI_hypothesis (L / M) (K / M) defWbar}%g.
proof: Proof. move=> ntW2bar sMK /andP[_ nML]. have coMW1: coprime #|M| #|W1| by rewrite (coprimeSg sMK). have [nMW1 nMW] := (subset_trans sW1L nML, subset_trans sWL nML). have defWbar: (W1 / M) \x (W2 / M) = (W / M)%g. by rewrite (quotient_coprime_dprod nMW) ?quotient_odd. exists defWbar; split; rewrite ?quotient_odd ?quotient_cyclic ?quotientS //. have isoW1: W1 \isog W1 / M by rewrite quotient_isog ?coprime_TIg. by rewrite -(isog_eq1 isoW1) ?morphim_Hall // (quotient_coprime_sdprod nML). move=> Kx /setD1P[ntKx /morphimP[x nKx W1x defKx]] /=. rewrite -cent_cycle -cycle_eq1 {Kx}defKx -quotient_cycle // in ntKx *. rewrite -strongest_coprime_quotient_cent ?cycle_subG //; first 1 last. - by rewrite subIset ?sMK. - by rewrite (coprimeSg (subsetIl M _)) // (coprimegS _ coMW1) ?cycle_subG. - by rewrite orbC abelian_sol ?cycle_abelian. rewrite cent_cycle prKW1 // !inE W1x (contraNneq _ ntKx) // => ->. by rewrite cycle1 quotient1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset fingroup) mathcomp(morphism perm automorphism quotient action gfunctor gproduct) mathcomp(center commutator zmodp cyclic pgroup nilpotent hall frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrnum algC classfun) mathcomp(character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3)