proposition: Lemma sub_path_except n n' m t (n'm : n' != m) : n' \notin t -> path (except n) m t -> path (except n') m t.
proof: Proof. move=> n't => /(pathP m) H; apply/(pathP m) => i it. move/H : (it); rewrite exceptE => /and3P[H1 _ _]. rewrite exceptE /= H1 /=. apply/andP; split; last by apply: contra n't => /eqP <-; rewrite mem_nth. move=> {H1}; case: i => [|i] in it *; first by apply: contra n'm => /eqP <-. apply: contra n't => /eqP <-; by rewrite /= mem_nth // ltnW. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext