proposition: Lemma Fgraph_m0 m0 n0 : n0 \in 'V m0 -> m0 \in 'F(m0, n0).
proof: Proof. move=> Hm0; by rewrite /Fgraph inE /subgraph inE -VnextE Hm0 connect0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) bigop_ext ssralg_ext f2 subgraph_partition