proposition: Lemma Fnext_Vnext_Vgraph m0 n0 : n0 \in 'V m0 -> 'V m0 :\ n0 \subset 'V(m0, n0) :\ n0.
proof: Proof. move=> m0Fn0; apply/subsetP => n1. rewrite in_setD1. case/andP => X1 X2. rewrite in_setD1 X1 /= !inE (negbTE X1) orFb -VnextE /= m0Fn0 /=. apply/connect1. rewrite exceptE /= -VnextE X2. by apply: contra X1 => /eqP [] ->. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) bigop_ext ssralg_ext f2 subgraph_partition