proposition: Lemma mxrank_in_factmod m (W : 'M_(m, n)) : (\rank (in_factmod W) + \rank U)%N = \rank (U + W).
proof: Proof. rewrite -in_factmod_addsK in_factmodE; set fU := in_factmod 1%:M. suffices <-: ((U + W) :&: kermx fU :=: U)%MS by rewrite mxrank_mul_ker. apply: eqmx_trans (capmx_idPr (addsmxSl U W)). apply: cap_eqmx => //; apply/eqmxP/rV_eqP => u. by rewrite (sameP sub_kermxP eqP) -in_factmodE 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)