proposition: Lemma bigcup_succ_set0 n1 m0 : \bigcup_(m1 in 'F n1 :\ m0) 'F(m1, n1) == set0 -> 'F n1 :\ m0 == set0.
proof: Proof. set goal := (X in _ -> X). case/boolP : ('F n1 :\ m0 == set0) => //. rewrite /goal. case/set0Pn => m1 Hm1. apply (@bigcup_set0 _ _ _ _ (fun x => 'F x :\ m0) _ m1); first by rewrite Hm1. apply/set0Pn; exists m1. rewrite Fgraph_m0 // -FnextE. by move: Hm1; rewrite !inE => /andP[]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) bigop_ext ssralg_ext f2 subgraph_partition