proposition: Lemma mxrank_Frobenius m n p q (A : 'M_(m, n)) B (C : 'M_(p, q)) : \rank (A *m B) + \rank (B *m C) <= \rank B + \rank (A *m B *m C).
proof: Proof. rewrite -{2}(mulmx_base (A *m B)) -mulmxA (eqmxMfull _ (col_base_full _)). set C2 := row_base _ *m C. rewrite -{1}(subnK (rank_leq_row C2)) -(mxrank_ker C2) addnAC leq_add2r. rewrite addnC -{1}(mulmx_base B) -mulmxA eqmxMfull //. set C1 := _ *m C; rewrite -{2}(subnKC (rank_leq_row C1)) leq_add2l -mxrank_ker. rewrite -(mxrankMfree _ (row_base_free (A *m B))). have: (row_base (A *m B) <= row_base B)%MS by rewrite !eq_row_base submxMl. case/submxP=> D defD; rewrite defD mulmxA mxrankMfree ?mxrankS //. by rewrite sub_kermx -mulmxA (mulmxA D) -defD -/C2 mulmx_ker. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)