proposition: Lemma pathpP x y : reflect (exists p, pathp x y p) (connect (--) x y).
proof: Proof. apply: (iffP idP) => [|[p] /andP[A /eqP B]]; last by apply/connectP; exists p. case/upathP => p /upathW ?. by exists p. Qed.
imports: HB(structures) Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij)