proposition: Lemma submatrix_mul m n p k l (A : 'M[R]_(m,n)) (B : 'M[R]_(n,p)) (f : 'I_k -> 'I_m) (g : 'I_l -> 'I_p): submatrix f g (A *m B) = (submatrix f id A) *m (submatrix id g B).
proof: Proof. apply/matrixP => i j; rewrite !mxE. by apply/eq_big => // x _; rewrite !mxE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice finfun matrix bigop zmodp poly mxpoly)