proposition: Lemma minor_alternate_f m n p (f : 'I_p -> 'I_m) g (M : 'M[R]_(m,n)) : (exists x y, (x != y) /\ (f x == f y)) -> minor f g M = 0.
proof: Proof. rewrite /minor => [[x [y [hxy /eqP hf]]]]. by rewrite (determinant_alternate hxy) // => a; rewrite !mxE hf. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq path ssralg) mathcomp(fintype perm choice finfun matrix bigop zmodp poly mxpoly)