fact: Definition known_port (p : graph_node) := match p with | inl x => x \in ports (nodes c) | inr y => y \in known_coports c end.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner