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