proposition: Lemma max_submod_eqmx U1 U2 V1 V2 : (U1 :=: U2)%MS -> (V1 :=: V2)%MS -> max_submod U1 V1 -> max_submod U2 V2.
proof: Proof. move=> eqU12 eqV12 [ltUV1 maxU1]. by split=> [|W]; rewrite -(lt_eqmx eqU12) -(lt_eqmx eqV12). 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)