proposition: Lemma ext_uniq_path (ac : acyclic') a b c s : uniq_path g b (c :: s) -> g a b -> a \notin s.
proof: Proof. move/andP => [Hp Hun] Hab; apply/negP => /splitPr Hsp. destruct Hsp. case Hli: (last b (c :: p1) == b). move/andP/proj1: Hun. by rewrite -cat_cons mem_cat -(eqP Hli) /= mem_last. suff: false by []; rewrite -Hli. apply (ac a b (c :: p1)). apply/negP => Ha. by rewrite (cat_uniq [:: b,c & p1] [:: a & p2]) /= Ha /= !andbF in Hun. rewrite -cat_rcons -cat_cons cat_path in Hp. move/andP/proj1: Hp => /= ->. by rewrite Hab. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix) ssr_ext