proposition: Lemma part_nodes_step_it c t : part (nodes (step_it c t)) = nodes c.
proof: Proof. rewrite /step_it. move: (enum _) => b. elim: b c t => [|s b IH] //= c t. by rewrite zip_nill. case: t => [|x t] //=. rewrite IH /=. rewrite /step_nodes. by case: ifP. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner