proposition: Lemma connect_except n w v : connect (except g n) w v -> connect g w v.
proof: Proof. case/connectP=> t wt ->{v}. case/shortenP : wt => t' wt' Hun t't. apply/connectP; exists t' => //. by apply: sub_path wt' => x y /except_rel. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext