proposition: Lemma tree_like_rev_subrel (c1 c2 : comp_graph port) : subrel (graph_rel c1) (graph_rel c2) -> tree_like c2 -> tree_like c1.
proof: Proof. move=> Hsub /'forall_forallP /= Htl. apply/'forall_forallP => /= n p. apply: contra (Htl n p). rewrite /ucycleb 2!(cycle_path (thead p)). by case/andP => /(sub_path Hsub) ->. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner