proposition: Lemma path_srev x p : path (--) x p = path (--) (last x p) (srev x p).
proof: Proof. rewrite rev_path [in RHS](eq_path (e' := (--))) //. move => {x} x y. exact: sg_sym. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)