proposition: Corollary tree_like_switch port (c : comp_graph port) : tree_like (switch c) = tree_like c.
proof: Proof. case Htl: (tree_like c). by apply tree_like_switch_imp. rewrite -(switchK c) in Htl. apply/contraFF: Htl. by apply tree_like_switch_imp. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner