proposition: Lemma neighbor_interiorL (G : sgraph) (x y : G) (p : Path x y) : x != y -> irred p -> neighbor [set x] (y |: interior p).
proof: Proof. move => xDy Ip. case: (set_0Vmem (interior p)) => [E|[z Hz]]. - apply: neighborUl. apply/neighborP; exists x; exists y. case: (interior0E xDy Ip E) => xy _. split => //; by rewrite inE eqxx. - apply: neighborUr. apply: path_neighborL => //; by set_tac. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)