proposition: Lemma monotonic_edom_step_it c t : edom c \subset edom (step_it c t).
proof: Proof. rewrite /step_it. move: (zip _ _) => {t} z. elim: z c => //= [] [p [ep en]] z IH c /=. by apply (subset_trans (monotonic_edom_step c p ep en)). Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner