proposition: Lemma path_except n h t : n \notin h :: t -> path g h t -> path (except n) h t.
proof: Proof. move=> nt /pathP H. apply/(pathP n) => i it; rewrite exceptE; apply/and3P; split; [by apply H | | ]. - apply: contra nt => /eqP <-. apply: mem_nth => /=; by rewrite ltnS ltnW. - apply: contra nt => /eqP <-; by rewrite inE mem_nth ?orbT. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext