proposition: Lemma last_rev_belast x y p : last x p = y -> last y (srev x p) = x.
proof: Proof. case: p => //= a p _. by rewrite /srev rev_cons last_rcons. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)