proposition: Lemma section_eqmx_add U1 U2 V1 V2 modU1 modU2 modV1 modV2 : (U1 :=: U2)%MS -> (U1 + V1 :=: U2 + V2)%MS -> mx_rsim (@section_repr U1 V1 modU1 modV1) (@section_repr U2 V2 modU2 modV2).
proof: Proof. move=> eqU12 eqV12; set n1 := {1}(\rank _). pose v1 := val_factmod (val_submod (1%:M : 'M_n1)). have sv12: (v1 <= U2 + V2)%MS. rewrite -eqV12 (submx_trans _ (proj_factmodS _ _)) //. by rewrite submxMr // val_submod1 genmxE. exists (v1 *m in_factmod _ 1%:M *m in_submod _ 1%:M) => [||x Gx]. - apply: (@addIn (\rank U1)); rewrite {2}eqU12 /n1 !{1}genmxE. by rewrite !{1}mxrank_in_factmod eqV12. - rewrite -kermx_eq0; apply/rowV0P=> u; rewrite (sameP sub_kermxP eqP) mulmxA. rewrite -in_submodE mulmxA -in_factmodE -(inj_eq val_submod_inj) linear0. rewrite in_submodK ?in_factmod_eq0 -?eqU12 => [U1uv1|]; last first. by rewrite genmxE -(in_factmod_addsK U2 V2) submxMr // mulmx_sub. apply: val_submod_inj; apply/eqP; rewrite linear0 -[val_submod _]val_factmodK. by rewrite in_factmod_eq0 val_factmodE val_submodE -mulmxA -val_factmodE. symmetry; rewrite -{1}in_submodE -{1}in_factmodE -{1}in_submodJ; last first. by rewrite genmxE -(in_factmod_addsK U2 V2) submxMr. rewrite -{1}in_factmodJ // mulmxA in_submodE; congr (_ *m _); apply/eqP. rewrite mulmxA -in_factmodE -subr_eq0 -linearB in_factmod_eq0 -eqU12. rewrite -in_factmod_eq0 linearB /= subr_eq0 {1}(in_factmodJ modU1) //. rewrite val_factmodK /v1 val_factmodE eq_sym mulmxA -val_factmodE val_factmodK. by rewrite -[_ *m _]mul1mx mulmxA -val_submodE val_submodJ. 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)