proposition: Lemma path_neighborR (G : sgraph) (x y : G) (p : Path x y) (A : {set G}) : irred p -> interior p != set0 -> y \in A -> neighbor A (interior p).
proof: Proof. move => Ip P0 yA. rewrite -interior_rev. apply: path_neighborL; by rewrite // ?irred_rev ?interior_rev. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph) GraphTheory(set_tac)