proposition: Lemma StrongJordanHolderUniqueness (G : {group rT}) (s1 s2 : seq {group rT}) : G \subset D -> acomps to G s1 -> acomps to G s2 -> perm_eq (mkfactors G s1) (mkfactors G s2).
proof: Proof. have [n] := ubnP #|G|; elim: n G => // n Hi G in s1 s2 * => cG hsD cs1 cs2. case/orP: (orbN (G :==: 1)) => [tG | ntG]. have -> : s1 = [::] by apply/eqP; rewrite -(trivg_acomps cs1). have -> : s2 = [::] by apply/eqP; rewrite -(trivg_acomps cs2). by rewrite /= perm_refl. case/orP: (orbN (asimple to G))=> [sG | nsG]. have -> : s1 = [:: 1%G ] by apply/(asimple_acompsP cs1). have -> : s2 = [:: 1%G ] by apply/(asimple_acompsP cs2). by rewrite /= perm_refl. case es1: s1 cs1 => [|N1 st1] cs1. by move: (trivg_comps cs1); rewrite eqxx; move/negP:ntG. case es2: s2 cs2 => [|N2 st2] cs2 {s1 es1}. by move: (trivg_comps cs2); rewrite eqxx; move/negP:ntG. case/andP: cs1 => /= lst1; case/andP=> maxN_1 pst1. case/andP: cs2 => /= lst2; case/andP=> maxN_2 pst2. have sN1D : N1 \subset D. by apply: subset_trans hsD; apply: maxainv_sub maxN_1. have sN2D : N2 \subset D. by apply: subset_trans hsD; apply: maxainv_sub maxN_2. have cN1 : #|N1| < n. by rewrite -ltnS (leq_trans _ cG) ?ltnS ?proper_card ?(maxainv_proper maxN_1). have cN2 : #|N2| < n. by rewrite -ltnS (leq_trans _ cG) ?ltnS ?proper_card ?(maxainv_proper maxN_2). case: (N1 =P N2) {s2 es2} => [eN12 |]. by rewrite eN12 /= perm_cons Hi // /acomps ?lst2 //= -eN12 lst1. move/eqP; rewrite -val_eqE /=; move/eqP=> neN12. have nN1G : N1 <| G by apply: (maxainv_norm maxN_1). have nN2G : N2 <| G by apply: (maxainv_norm maxN_2). pose N := (N1 :&: N2)%G. have nNG : N <| G. by rewrite /normal subIset ?(normal_sub nN1G) //= normsI ?normal_norm. have iso1 : (G / N1)%G \isog (N2 / N)%G. rewrite isog_sym /= -(maxainvM _ _ maxN_1 maxN_2) //. rewrite (@normC _ N1 N2) ?(subset_trans (normal_sub nN1G)) ?normal_norm //. by rewrite weak_second_isog ?(subset_trans (normal_sub nN2G)) ?normal_norm. have iso2 : (G / N2)%G \isog (N1 / N)%G. rewrite isog_sym /= -(maxainvM _ _ maxN_1 maxN_2) // setIC. by rewrite weak_second_isog ?(subset_trans (normal_sub nN1G)) ?normal_norm. case: (exists_acomps to N)=> sN; case/andP=> lsN csN. have aN1 : [acts A, on N1 | to]. by case/maxgroupP: maxN_1; case/and3P. have aN2 : [acts A, on N2 | to]. by case/maxgroupP: maxN_2; case/and3P. have nNN1 : N <| N1. by apply: (normalS _ _ nNG); rewrite ?subsetIl ?normal_sub. have nNN2 : N <| N2. by apply: (normalS _ _ nNG); rewrite ?subsetIr ?normal_sub. have aN : [ acts A, on N1 :&: N2 | to]. apply/subsetP=> x Ax; rewrite !inE Ax /=; apply/subsetP=> y Ny; rewrite inE. case/setIP: Ny=> N1y N2y. rewrite inE ?astabs_act ?N1y ?N2y //. by move/subsetP: aN2; move/(_ x Ax). by move/subsetP: aN1; move/(_ x Ax). have i1 : perm_eq (mksrepr G N1 :: mkfactors N1 st1) [:: mksrepr G N1, mksrepr N1 N & mkfactors N sN]. rewrite perm_cons -[mksrepr _ _ :: _]/(mkfactors N1 [:: N & sN]). apply: Hi=> //; rewrite /acomps ?lst1 //= lsN csN andbT /=. apply: asimple_quo_maxainv=> //; first by apply: subIset; rewrite sN1D. apply: asimpleI => //. by apply: subset_trans (normal_norm nN2G); apply: normal_sub. rewrite -quotientMidl (maxainvM _ _ maxN_2) //. by apply: maxainv_asimple_quo. by move=> e; apply: neN12. have i2 : perm_eq (mksrepr G N2 :: mkfactors N2 st2) [:: mksrepr G N2, mksrepr N2 N & mkfactors N sN]. rewrite perm_cons -[mksrepr _ _ :: _]/(mkfactors N2 [:: N & sN]). apply: Hi=> //; rewrite /acomps ?lst2 //= lsN csN andbT /=. apply: asimple_quo_maxainv=> //; first by apply: subIset; rewrite sN1D. have e : N1 :&: N2 :=: N2 :&: N1 by rewrite setIC. rewrite (group_inj (setIC N1 N2)); apply: asimpleI => //. by apply: subset_trans (normal_norm nN1G); apply: normal_sub. rewrite -quotientMidl (maxainvM _ _ maxN_1) //. exact: maxainv_asimple_quo. pose fG1 := [:: mksrepr G N1, mksrepr N1 N & mkfactors N sN]. pose fG2 := [:: mksrepr G N2, mksrepr N2 N & mkfactors N sN]. have i3 : perm_eq fG1 fG2. rewrite (@perm_catCA _ [::_] [::_]) /mksrepr. rewrite (@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso1). rewrite -(@section_repr_isog _ (mkSec _ _) (mkSec _ _) iso2). exact: perm_refl. apply: (perm_trans i1); apply: (perm_trans i3); rewrite perm_sym. by apply: perm_trans i2; apply: perm_refl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype bigop finset fingroup morphism) mathcomp(automorphism quotient action gseries)