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