proposition: Lemma path_except_neq n m h l : m \in l -> path (except n) h l -> n != m.
proof: Proof. elim: l n m h => // a b IH n m h; rewrite in_cons => /orP[/eqP <-{a}|mb] /=. by case/andP => /except13. by case/andP => H1 /(IH _ _ _ mb). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext