proposition: Lemma subgraph_connect n v w : g n w -> v \in subgraph w n -> connect g n v.
proof: Proof. move=> nw; rewrite /subgraph inE nw /= => wv. move/connect1 : nw => /connect_trans; apply. exact: connect_except wv. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext