proposition: Lemma rcons_pathp x y p : path (--) x (rcons p y) = pathp x y (rcons p y).
proof: Proof. by rewrite /pathp last_rcons eqxx andbT. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)