proposition: Lemma upath_sym x y : unique (upath x y) -> unique (upath y x).
proof: Proof. move => U p q Hp Hq. suff S: last y p = last y q. { apply: last_belast_eq S _; apply: rev_inj; apply: U; exact: rev_upath. } rewrite !(@pathp_last _ x) //; exact: upathW. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)