proposition: Lemma minor_ltn_eq0l k m1 m2 n1 n2 x (f : 'I_k -> 'I_(m1 + m2)) g (M : 'M[R]_(m1,n1)) (N : 'M_(m1,n2)) (H : m1 < f x) : minor f g (block_mx M N 0 0) = 0.
proof: Proof. rewrite /minor (expand_det_row _ x) big1 // => i _; rewrite !mxE. case: splitP H => [j ->|j Hj]; first by rewrite ltnNge ltnW. by rewrite row_mx0 mxE mul0r. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice finfun matrix bigop zmodp poly mxpoly)