proposition: Lemma sub_submatrix k k' l l' m n (M : 'M[A]_(m,n)) (f' : 'I_k -> 'I_m) (f : 'I_k' -> 'I_k) (g' : 'I_l -> 'I_n) (g : 'I_l' -> 'I_l) : submatrix f g (submatrix f' g' M) = submatrix (f' \o f) (g' \o g) 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)