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