proposition: Lemma bigcup_Fgraph_set0 m0 n0 : [set \bigcup_(m1 in 'F n1 :\ m0) 'F(m1, n1) | n1 in 'V m0 :\ n0] == set0 -> 'V m0 :\ n0 == set0.
proof: Proof. move/set0Pn => abs; apply/set0Pn => -[n1 Hn1 /=]; apply abs => {abs}. exists (\bigcup_(m1 in 'F n1 :\ m0) 'F(m1, n1)). by apply/imsetP; exists n1. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) bigop_ext ssralg_ext f2 subgraph_partition