proposition: Lemma mx_rsim_factmod n (rG : reprG n) U V (modU : mxmodule rG U) (modV : mxmodule rG V) : (U + V :=: 1%:M)%MS -> mxdirect (U + V) -> mx_rsim (factmod_repr modV) (submod_repr modU).
proof: Proof. move=> addUV dxUV. have eqUV: \rank U = \rank (cokermx V). by rewrite mxrank_coker -{3}(mxrank1 F n) -addUV (mxdirectP dxUV) addnK. have{} dxUV: (U :&: V = 0)%MS by apply/mxdirect_addsP. exists (in_submod U (val_factmod 1%:M *m proj_mx U V)) => // [|x Gx]. rewrite /row_free -{6}eqUV -[_ == _]sub1mx -val_submodS val_submod1. rewrite in_submodK ?proj_mx_sub // -{1}[U](proj_mx_id dxUV) //. rewrite -{1}(add_sub_fact_mod V U) mulmxDl proj_mx_0 ?val_submodP // add0r. by rewrite submxMr // val_factmodS submx1. rewrite -in_submodJ ?proj_mx_sub // -(hom_mxP _) //; last first. by apply: submx_trans (submx1 _) _; rewrite -addUV proj_mx_hom. rewrite mulmxA; congr (_ *m _); rewrite mulmxA -val_factmodE; apply/eqP. rewrite eq_sym -subr_eq0 -mulmxBl proj_mx_0 //. by rewrite -[_ *m rG x](add_sub_fact_mod V) addrK val_submodP. 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)