proposition: Lemma JordanHolderUniqueness (G : gTg) (s1 s2 : seq gTg) : comps G s1 -> comps 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 * => /ltnSE-cG cs1 cs2. have [G1 | ntG] := boolP (G :==: 1). have -> : s1 = [::] by apply/eqP; rewrite -(trivg_comps cs1). have -> : s2 = [::] by apply/eqP; rewrite -(trivg_comps cs2). by rewrite /= perm_refl. have [sG | nsG] := boolP (simple G). by rewrite (simple_compsP cs1 sG) (simple_compsP cs2 sG) 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 cN1 : #|N1| < n. by rewrite (leq_trans _ cG) ?proper_card ?(maxnormal_proper maxN_1). have cN2 : #|N2| < n. by rewrite (leq_trans _ cG) ?proper_card ?(maxnormal_proper maxN_2). case: (N1 =P N2) {s2 es2} => [eN12 |]. by rewrite eN12 /= perm_cons Hi // /comps ?lst2 //= -eN12 lst1. move/eqP; rewrite -val_eqE /=; move/eqP=> neN12. have nN1G : N1 <| G by apply: maxnormal_normal. have nN2G : N2 <| G by apply: maxnormal_normal. 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 /= -(maxnormalM 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 /= -(maxnormalM maxN_1 maxN_2) // setIC. by rewrite weak_second_isog ?(subset_trans (normal_sub nN1G)) ?normal_norm. have [sN /andP[lsN csN]] := exists_comps N. 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 /comps ?lst1 //= lsN csN andbT /=. rewrite -quotient_simple. by rewrite -(isog_simple iso2) quotient_simple. by rewrite (normalS (subsetIl N1 N2) (normal_sub nN1G)). 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 /comps ?lst2 //= lsN csN andbT /=. rewrite -quotient_simple. by rewrite -(isog_simple iso1) quotient_simple. by rewrite (normalS (subsetIr N1 N2) (normal_sub nN2G)). 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)