proposition: Lemma tree_like_start i : tree_like (start_graph i).
proof: Proof. apply/'forall_forallP => n. rewrite /ucycleb /cycle. case => /=. case => // s1. case => //= [|s2]. by case: s1 => [] [] s1 []. case => //= [|s3 s] _. case: s1 => [] [] s1 [] //=; case: s2 => [] [] s2 [] //=; by rewrite !andbF. case: s1 => [] [] s1 [] //=; case: s2 => [] [] s2 [] //=; try by rewrite !andbF. - rewrite inE /= /ports big_set1. by case: (s1 \in i). - case: existsP => //= [] [j]. rewrite inE => /and4P[/eqP -> {j} H1 H2 H3]. case: s3 => [] [] s3 [] //=; try by rewrite !andbF. rewrite inE /= /ports big_set1. by case: (s2 \in i). - rewrite inE /= /ports big_set1. by case: (s2 \in i). - case: existsP => //= [] [j]. by rewrite inE. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup zmodp poly ssrnum) mathcomp(matrix perm) ssr_ext ssralg_ext fdist subgraph_partition tanner