proposition: Lemma tree_like_rev_step_it (c : comp_graph port) t : tree_like (step_it c t) -> tree_like c.
proof: Proof. apply tree_like_rev_subrel. rewrite /step_it. elim: t c (enum _) => [|[ep en] t IH] /= c [] s b //=. apply (@subrel_trans _ (graph_rel (step c s ep en))). apply monotonic_step_rel. apply IH. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner