proposition: Lemma upathPR (G : diGraph) (x y : G) A : reflect (exists p : seq G, @upath (drestrict A) x y p) (connect (restrict A (--)) x y).
proof: Proof. exact: (@upathP (drestrict A)). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)