proposition: Lemma tree_like_rev_switch_step_it (c : comp_graph port) t : tree_like (switch_step_it c t) -> tree_like c.
proof: Proof. elim: t c => [//|[epen] t IH] /= c Htl. set s := map _ _ in Htl. apply (@tree_like_rev_step_it c s). by rewrite -tree_like_switch IH. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner