proposition: Lemma acyclic_equiv : acyclic' <-> acyclic.
proof: Proof. rewrite /acyclic' /acyclic; split => [Hac | ]. case=> [// | a [// | b [// | c p _ /= /andP[Hcp]]]]. rewrite [ [:: b, c & p] ]lock /= -lock => /andP[abcp]. have /eqP H : last b (c :: p) == b by move/Hac : abcp; apply. by rewrite /= -H /= mem_last. move=> Hac a b p Ha. rewrite /path.cycle rcons_path => /andP [/=/andP[Hab Hp]]. case : {Hp}(shortenP Hp) => p' Hp' Hun Hmem Hla. move: {Hac}(Hac [:: a, b & p']). rewrite /ucycle /cycle {3}[b :: p']lock /= -lock Hun Hab rcons_path Hp' Hla. rewrite (_ : a \notin b :: p'); last first. apply: contra Ha; rewrite !inE => /orP[/eqP ->|]; first by rewrite eqxx. by move/Hmem; rewrite ?inE => ->; rewrite orbT. by destruct p' as [|p'1 p'2] => [//|/= /(_ isT)]. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext