proposition: Lemma mx_JordanHolder U V compU compV : let m := size U in (last 0 U :=: last 0 V)%MS -> m = size V /\ (exists p : 'S_m, forall i : 'I_m, mx_rsim (@series_repr U i compU) (@series_repr V (p i) compV)).
proof: Proof. move Dr: {-}(size U) => r; move/eqP in Dr. elim: r U V Dr compU compV => /= [|r IHr] U V. move/nilP->; case/lastP: V => [|V Vm] /= ? compVm; rewrite ?last_rcons => Vm0. by split=> //; exists 1%g; case. by case/mx_series_rcons: (compVm) => _ _ []; rewrite -(lt_eqmx Vm0) ltmx0. case/lastP: U => // [U Um]; rewrite size_rcons eqSS => szUr compUm. case/mx_series_rcons: (compUm); set Um' := last 0 U => compU modUm maxUm. case/lastP: V => [|V Vm] compVm; rewrite ?last_rcons ?size_rcons /= => eqUVm. by case/mx_series_rcons: (compUm) => _ _ []; rewrite (lt_eqmx eqUVm) ltmx0. case/mx_series_rcons: (compVm); set Vm' := last 0 V => compV modVm maxVm. have [modUm' modVm']: modG Um' * modG Vm' := (last_mod compU, last_mod compV). pose i_m := @ord_max (size U). have [eqUVm' | neqUVm'] := altP (@eqmxP _ _ _ _ Um' Vm'). have [szV [p sim_p]] := IHr U V szUr compU compV eqUVm'. split; first by rewrite szV. exists (lift_perm i_m i_m p) => i; case: (unliftP i_m i) => [j|] ->{i}. apply: rsimT (rsimC _) (rsimT (sim_p j) _). by rewrite lift_max; apply: rsim_rcons. by rewrite lift_perm_lift lift_max; apply: rsim_rcons; rewrite -szV. have simUVm := section_eqmx modUm' modVm' modUm modVm eqUVm' eqUVm. apply: rsimT (rsimC _) (rsimT simUVm _); first exact: rsim_last. by rewrite lift_perm_id /= szV; apply: rsim_last. have maxVUm: max_submod Vm' Um by apply: max_submod_eqmx (eqmx_sym _) maxVm. have:= mx_butterfly modUm' modVm' modUm neqUVm' maxUm maxVUm. move: (capmx_module _ _); set Wm := (Um' :&: Vm')%MS => modWm [maxWUm simWVm]. have:= mx_butterfly modVm' modUm' modUm _ maxVUm maxUm. move: (capmx_module _ _); rewrite andbC capmxC -/Wm => modWmV [// | maxWVm]. rewrite {modWmV}(bool_irrelevance modWmV modWm) => simWUm. have [W compW lastW] := mx_JordanHolder_exists compU modWm maxWUm. have compWU: mx_series (rcons W Um') by apply/mx_series_rcons; rewrite lastW. have compWV: mx_series (rcons W Vm') by apply/mx_series_rcons; rewrite lastW. have [|szW [pU pUW]] := IHr U _ szUr compU compWU; first by rewrite last_rcons. rewrite size_rcons in szW; have ltWU: size W < size U by rewrite -szW. have{IHr} := IHr _ V _ compWV compV; rewrite last_rcons size_rcons -szW. case=> {r szUr}// szV [pV pWV]; split; first by rewrite szV. pose j_m := Ordinal ltWU; pose i_m' := lift i_m j_m. exists (lift_perm i_m i_m pU * tperm i_m i_m' * lift_perm i_m i_m pV)%g => i. rewrite !permM; case: (unliftP i_m i) => [j {simWUm}|] ->{i}; last first. rewrite lift_perm_id tpermL lift_perm_lift lift_max {simWVm}. apply: rsimT (rsimT (pWV j_m) _); last by apply: rsim_rcons; rewrite -szV. apply: rsimT (rsimC _) {simWUm}(rsimT simWUm _); first exact: rsim_last. by rewrite -lastW in modWm *; apply: rsim_last. apply: rsimT (rsimC _) {pUW}(rsimT (pUW j) _). by rewrite lift_max; apply: rsim_rcons. rewrite lift_perm_lift; case: (unliftP j_m (pU j)) => [k|] ->{j pU}. rewrite tpermD ?(inj_eq lift_inj) ?neq_lift //. rewrite lift_perm_lift !lift_max; set j := lift j_m k. have ltjW: j < size W by have:= ltn_ord k; rewrite -(lift_max k) /= {1 3}szW. apply: rsimT (rsimT (pWV j) _); last by apply: rsim_rcons; rewrite -szV. by apply: rsimT (rsimC _) (rsim_rcons compW _ _); first apply: rsim_rcons. apply: rsimT {simWVm}(rsimC (rsimT simWVm _)) _. by rewrite -lastW in modWm *; apply: rsim_last. rewrite tpermR lift_perm_id /= szV. by apply: rsimT (rsim_last modVm' modVm _); apply: section_eqmx. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)