proposition: Lemma Fgraph_nonempty m1 n1 : n1 \notin 'V m1 -> 'F(m1, n1) == set0.
proof: Proof. move=> m1n1. apply/eqP/setP => m2. rewrite in_set0. apply/negbTE. apply: contra m1n1. rewrite 2!inE -VnextE; by case/andP. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) bigop_ext ssralg_ext f2 subgraph_partition