proposition: Lemma mem_prev x y (p : Path x y) u : (u \in prev p) = (u \in p).
proof: Proof. rewrite !mem_path !nodesE -srev_nodes //. exact: valP. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)