fact: Record hemi_comp_graph := { part :> {set {set port}} ; part_p : trivIset part ; border : {set port} ; ports := \bigcup_(x in part) x; border_p : border \subset ports; }.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner