proposition: Lemma rev_upath x y p : upath x y p -> upath y x (srev x p).
proof: Proof. case/andP => A B. apply/andP; split; last exact: pathp_rev. apply: leq_size_uniq A _ _. - move => z. by rewrite -srev_nodes. - by rewrite /= size_rev size_belast. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)