fact: Definition comp_graph_eqb (c1 c2 : comp_graph) := [&& nodes c1 == nodes c2, conodes c1 == conodes c2 & edges c1 == edges c2].
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner