proposition: Lemma Vgraph_set1 m1 n1 : n1 \notin 'V m1 -> 'V(m1, n1) = [set n1].
proof: Proof. move=> m1n1. apply/setP => n2. rewrite inE in_set1 /=. case/boolP: (n2 == n1) => //= n2n1. by rewrite 2!inE -VnextE (negbTE m1n1). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) bigop_ext ssralg_ext f2 subgraph_partition