fact: Definition dest_ports c len := [set x : len.-tuple (port * {set port})%type | [&& all (fun i => i.1 \in i.2 :\: graph_dom (conodes c)) x, uniq (unzip1 x) & trivIset ([set y in unzip2 x] :|: conodes c)]].
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner