fact: Definition start_dist (pn : {set port}) := if #|pn| == 0%nat then 0 else lam`_#|pn|.-1 / ('C(#|port|, #|pn|))%:R.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner