fact: Definition Fgraph_part_Fgraph m0 n0 : {set {set 'I_m}} := (fun n1 => \bigcup_(m1 in 'F n1 :\ m0) 'F(m1, n1)) @: (('V m0) :\ n0).
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) mathcomp(Rstruct) ssr_ext subgraph_partition tanner f2