proposition: Lemma edgeLP x y z (xy : x -- y) (p : Path y z) u : reflect (u = x \/ u \in p) (u \in pcat (edgep xy) p).
proof: Proof. rewrite mem_pcat mem_edgep -orbA. apply: (iffP or3P) => [|[->|->]]; rewrite ?eqxx. 1: case => [/eqP->|/eqP->|->]; rewrite ?inE. all: by firstorder using path_begin. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)