proposition: Lemma path_neighborL (G : sgraph) (x y : G) (p : Path x y) (A : {set G}) : irred p -> interior p != set0 -> x \in A -> neighbor A (interior p).
proof: Proof. move => Ip /set0Pn [z Hz] xA. have xDy : x != y. { apply: contraTneq Hz => ?; subst y. rewrite (irredxx Ip). rewrite !inE mem_idp. by case: (z == x). } case: (splitL p xDy) => u [xu] [p'] [E _]. rewrite E irred_edgeL in Ip. apply/neighborP; exists x; exists u; split => //. case/andP : Ip => Hp Ip. rewrite E !inE /= andbT eq_sym sg_edgeNeq //=. apply: contraTneq Hz => ?. subst u. by rewrite E (irredxx Ip) pcat_idR interior_edgep inE. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)