proposition: Lemma submatrix_lift_block m n p q (f1 : 'I_p -> 'I_m) (f2 : 'I_q -> 'I_n) a (M: 'M[R]_(m,n)) (c : 'cV[R]_m) (l : 'rV[R]_n) : submatrix (lift_pred f1) (lift_pred f2) (block_mx a%:M l c M) = block_mx a%:M (submatrix id f2 l) (submatrix f1 id c) (submatrix f1 f2 M).
proof: Proof. apply/matrixP => i j; rewrite !mxE /lift_pred !split1. case: (oapp _ _ (unlift 0 i)) => x. rewrite unlift_none /= [x]ord1 !mxE !split1. case: (oapp _ _ (unlift 0 j)) => y; first by rewrite unlift_none [y]ord1. by rewrite liftK mxE. rewrite liftK /= !mxE !split1. case: (oapp _ _ (unlift 0 j)) => y; first by rewrite unlift_none mxE [y]ord1. by rewrite liftK mxE. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice finfun matrix bigop zmodp poly mxpoly)