proposition: Lemma uncycle x y (p : Path x y) : exists2 p' : Path x y, {subset p' <= p} & irred p'.
proof: Proof. case: p => p pth_p. case/pathp_shorten : (pth_p) => p' [A B C]. exists (Build_Path A). move => z. rewrite !mem_path !nodesE !SubK. + rewrite !inE. case/predU1P => [->|/C ->] //. by rewrite eqxx. + by rewrite /irred nodesE. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)