fact: Definition dest_dist (dn : {set port}) : K := if dn \in conodes c then 1 else (lambda `_ #|dn|.-1) / ('C(#|port|.-1 - #|known_coports c|, #|dn|.-1))%:R.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner