proposition: Lemma Fgraph_Vnext2_Vgraph m0 n0 m1 n1 : m1 \in 'F(m0, n0) -> n1 \in 'V m1 -> n0 \in 'V m0 -> n1 \in 'V(m0, n0).
proof: Proof. move=> Hm1 Hn1 Hm0. apply/negPn/negP. rewrite !inE negb_or. case/andP => n1n0. rewrite !inE in Hm1, Hm0. rewrite negb_and /= -VnextE Hm0 /=. case/andP : Hm1 => _ Hm1 abs. move/negP : abs; apply. apply: (@connect_trans _ _ (inl m1) _ _ Hm1). apply/connect1. rewrite exceptE /= -VnextE Hn1 /=. by apply: contra n1n0 => /eqP [] ->. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) bigop_ext ssralg_ext f2 subgraph_partition