proposition: Lemma minor_eq0l (R : comRingType) k1 m1 n1 (s1 : seq R) x : forall (f : 'I_k1 -> 'I_m1) g, (n1 <= f x)%N -> minor f g (diag_mx_seq m1 n1 s1) = 0.
proof: Proof. move=> f g H. rewrite /minor (expand_det_row _ x) big1 // => i _. by rewrite !mxE gtn_eqF ?mul0r // (leq_trans _ H). Qed.
imports: mathcomp(all_ssreflect) mathcomp(all_algebra) mathcomp(all_fingroup) mathcomp(all_real_closed) CoqEAL(binetcauchy ssrcomplements mxstructure minor) CoqEAL(smith dvdring polydvd) CoqEAL(similar perm_eq_image)