proposition: Lemma irred_is_edge (x y : D) (p : Path x y) : irred p -> x != y -> {subset p <= [set x;y]} -> exists xy : x -- y, p = edgep xy.
proof: Proof. move => Ip xDy sub_xy. case: (splitL p xDy) => y' [xy'] [p' [def_p _]]. subst. move: Ip. rewrite irred_edgeL => /andP[xp' Ip']. suff ? : y' = y. { subst. rewrite [p']irredxx // pcat_idR. by exists xy'. } move/(_ y') : sub_xy. rewrite mem_pcat path_begin orbT !inE => /(_ isT). case/orP => /eqP ?; subst => //. by rewrite path_begin in xp'. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)