proposition: Lemma submatrix_eq m n p q (f1 g1 : 'I_p -> 'I_m) (f2 g2 : 'I_q -> 'I_n) (M : 'M[R]_(m,n)) (h1 : f1 =1 g1) (h2 : f2 =1 g2) : submatrix f1 f2 M = submatrix g1 g2 M.
proof: Proof. by apply/matrixP => i j; rewrite !mxE (h1 i) (h2 j). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice finfun matrix bigop zmodp poly mxpoly)