fact: Definition single_hemi_graph (pn : {set port}) : hemi_comp_graph port := @Build_hemi_comp_graph _ [set pn] (trivIset1 _) pn (subset_cover1 _).
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner