proposition: Lemma submatrix0 n m p q (f1 : 'I_p -> 'I_m) (f2 : 'I_q -> 'I_n) : submatrix f1 f2 0 = 0 :> 'M[R]__.
proof: Proof. by 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)