fact: Fixpoint switch_step_it c (ts : seq {ffun port -> port * {set port}}) := match ts with | [::] => c | t :: ts => let b := enum (border (nodes c)) in let c' := step_it c (map t b) in switch_step_it (switch c') ts end.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner