proposition: Lemma Fgraph_Vnext_Vgraph m0 n0 m1 n1 : m1 \in 'F(m0, n0) -> n1 \in 'V m1 -> n1 != n0 -> n1 \in 'V(m0, n0).
proof: Proof. rewrite !inE /=. case/andP => m0n0 m0m1 m1n1 n1n0. rewrite (negbTE n1n0) m0n0 /=. apply/connectP => /=. case/connectP : m0m1 => /= p Hp1 Hp2. exists (rcons p (inr n1)). rewrite rcons_path /=. apply/andP; split => //. rewrite -Hp2. rewrite exceptE /= -VnextE m1n1 /=. by apply: contra n1n0 => /eqP [] ->. by rewrite last_rcons. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) bigop_ext ssralg_ext f2 subgraph_partition