proposition: Lemma Path_connect x y (p : Path x y) : connect (--) x y.
proof: Proof. apply/pathpP. exists (val p). exact: valP. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)