proposition: Lemma srevK x y p : last x p = y -> srev y (srev x p) = p.
proof: Proof. elim/last_ind: p => // p z _. by rewrite last_rcons !srev_rcons revK => ->. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)