proposition: Lemma path_except_notin n m l : path (except n) m l -> n \notin l.
proof: Proof. move=> Hpath; apply/negP => /(nthP m) [i il ni]. move/pathP : Hpath => /(_ m _ il); rewrite ni; apply/negP. by rewrite exceptN. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext