proposition: Lemma srev_nodes x y p : pathp x y p -> x :: p =i y :: srev x p.
proof: Proof. elim/last_ind: p => //; first by move/pathp_nil ->. move => p z _ H a. rewrite srev_rcons !(inE,mem_rcons,mem_rev). rewrite (pathp_rcons H). by case: (a == x). Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)