fact: Definition step_it (c : comp_graph port) d := let b := enum (border (nodes c)) in foldl (fun c x => step c x.1 x.2.1 x.2.2) c (zip b d).
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner