proposition: Lemma minorn n (A : 'M[R]_n) : minor id id A = \det A.
proof: Proof. by rewrite /minor /submatrix; congr (\det _); 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)