proposition: Lemma start_in_subgraph n m : g n m -> m \in subgraph m n.
proof: Proof. by move=> gnm; rewrite /subgraph inE gnm /= connect0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext