proposition: Lemma max_submodP U V (modU : modG U) (modV : modG V) : (U <= V)%MS -> (max_submod U V <-> mx_irreducible (section_repr modU modV)).
proof: Proof. move=> sUV; split=> [[ltUV maxU] | ]. apply/mx_irrP; split=> [|WU modWU nzWU]. by rewrite genmxE lt0n mxrank_eq0 in_factmod_eq0; case/andP: ltUV. rewrite -sub1mx -val_submodS val_submod1 genmxE. pose W := (U + val_factmod (val_submod WU))%MS. suffices sVW: (V <= W)%MS. rewrite {2}in_factmodE (submx_trans (submxMr _ sVW)) //. rewrite addsmxMr -!in_factmodE val_factmodK. by rewrite ((in_factmod U U =P 0) _) ?adds0mx ?in_factmod_eq0. move/and3P: {maxU}(maxU W); apply: contraR; rewrite /ltmx addsmxSl => -> /=. move: modWU; rewrite /mxmodule rstabs_submod rstabs_factmod => -> /=. rewrite addsmx_sub submx_refl -in_factmod_eq0 val_factmodK. move: nzWU; rewrite -[_ == 0](inj_eq val_submod_inj) linear0 => ->. rewrite -(in_factmodsK sUV) addsmxS // val_factmodS. by rewrite -(genmxE (in_factmod U V)) val_submodP. case/mx_irrP; rewrite lt0n {1}genmxE mxrank_eq0 in_factmod_eq0 => ltUV maxV. split=> // [|W [modW /andP[sUW ltUW] /andP[sWV /negP[]]]]; first exact/andP. rewrite -(in_factmodsK sUV) -(in_factmodsK sUW) addsmxS // val_factmodS. rewrite -genmxE -val_submod1; set VU := <<_>>%MS. have sW_VU: (in_factmod U W <= VU)%MS. by rewrite genmxE -val_factmodS !submxMr. rewrite -(in_submodK sW_VU) val_submodS -(genmxE (in_submod _ _)). rewrite sub1mx maxV //. rewrite (eqmx_module _ (genmxE _)) in_submod_module ?genmxE ?submxMr //. by rewrite in_factmod_module addsmx_module. rewrite -submx0 [(_ <= 0)%MS]genmxE -val_submodS linear0 in_submodK //. by rewrite eqmx0 submx0 in_factmod_eq0. 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)