proposition: Lemma pathp_rcons x y z p: pathp x y (rcons p z) -> y = z.
proof: Proof. case/andP => _ /eqP <-. exact: last_rcons. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)