proposition: Lemma rstabs_factmod m (W : 'M_(m, \rank (cokermx U))) : rstabs rU' W = rstabs rG (U + val_factmod W)%MS.
proof: Proof. apply/setP=> x /[!inE]; apply: andb_id2l => Gx. rewrite addsmxMr addsmx_sub (submx_trans (mxmoduleP Umod x Gx)) ?addsmxSl //. rewrite -val_factmodS val_factmodJ //= val_factmodS; apply/idP/idP=> nWx. rewrite (submx_trans (addsmxSr U _)) // -(in_factmodsK (addsmxSl U _)) //. by rewrite addsmxS // val_factmodS in_factmod_addsK. rewrite in_factmodE (submx_trans (submxMr _ nWx)) // -in_factmodE. by rewrite in_factmod_addsK val_factmodK. 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)