proposition: Lemma prevK x y (p : Path x y) : prev (prev p) = p.
proof: Proof. apply/val_inj=> /=. apply: srevK. exact: path_last. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)