proposition: Lemma drestrict_upath (G : diGraph) (x y : G) (A : pred G) (p : seq G) : @upath (@drestrict G A) x y p -> @upath G x y p.
proof: Proof. elim: p x => // z p IH x /upath_consE [/= /andP [_ u1] u2 u3]. rewrite upath_cons u1 u2 /=. exact: IH. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)