proposition: Lemma nodes_prev (x y : G) (p : Path x y) : nodes (prev p) = rev (nodes p).
proof: Proof. apply: rev_inj. rewrite /prev /srev !nodesE /=. by rewrite rev_cons !revK -{2}[y](path_last p) -lastI. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)