proposition: Lemma monotonic_edges_step_it c t : {in edom c, edges (step_it c t) =1 edges c}.
proof: Proof. rewrite /step_it. move: (zip _ _) => {t} z. elim: z c => //= [] [ep en] z IH c p Hp. rewrite IH /=. by rewrite monotonic_edges_step. by move: Hp; apply/subsetP/monotonic_edom_step. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner