proposition: Lemma submatrix_opp m n p k (A : 'M[R]_(m,n)) (f : 'I_p -> 'I_m) (g : 'I_k -> 'I_n) : submatrix f g (- A) = - submatrix f g A.
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)