proposition: Lemma srev_rcons x z p : srev x (rcons p z) = rcons (rev p) x.
proof: Proof. by rewrite /srev belast_rcons rev_cons. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)