proposition: Lemma prev_cat x y z (p : Path x y) (q : Path y z) : prev (pcat p q) = pcat (prev q) (prev p).
proof: Proof. apply/eqP. by rewrite -val_eqE /= /srev belast_cat rev_cat path_last. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)