proposition: Lemma connect_inE (T : finType) (e : rel T) (A : pred T) (x y : T) : x != y -> connect (restrict A e) x y -> (exists p, [/\ path e x (rcons p y), uniq (x::rcons p y) & {subset x::rcons p y <= A}]).
proof: Proof. move => xDy. case/(@upathPR (DiGraph e)) => p U. move/upath_rconsE : (drestrict_upath U) => -/(_ xDy) [P1 P2]. have E : last x p = y by case/andP : U => _; apply: pathp_last. rewrite -E -lastI in P2. exists (behead (belast x p)); split => //. - suff -> : rcons (behead (belast x p)) y = p by []. destruct p; rewrite -?E -?lastI //=. by rewrite -E /= eqxx in xDy. - move/upath_rconsE : (U) => /(_ xDy) => -[P _]. apply/cons_subset; split; last exact: rpath_sub P. destruct p; simpl in *. by rewrite E eqxx in xDy. case/upath_consE : U => /=. by rewrite /edge_rel/=; case: (x \in A). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)