proposition: Lemma monotone_conodes_step_it c t : conodes c \subset conodes (step_it c t).
proof: Proof. rewrite /step_it. move: (zip _ _) => z. elim: z c => //= a l IH c. rewrite (subset_trans _ (IH _)) //=. rewrite /step_conodes. destruct Bool.bool_dec => //. destruct step_cond => //=. apply subsetU1. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner