proposition: Theorem tree_like_switch_imp : tree_like c -> tree_like (switch c).
proof: Proof. move/'forall_forallP => Hc. apply/'forall_forallP => /= n p. move/(_ n (map_tuple switch_path_node p)) : Hc. apply: contra. rewrite /ucycleb /ucycle -(@cycle_morph _ (graph_rel (switch c))). rewrite map_inj_in_uniq //. move=> ? ? _ _; exact: inj_switch_path_node. move=> [x a] [y b]. by rewrite -switch_graph_rel /switch_path_node !switch_graph_nodeK. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner