proposition: Lemma disjoint_subpath (T : finType) (A B : pred T) (e : rel T) x y (p : seq T) : x \in A -> y \in B -> path e x (rcons p y) -> [disjoint A & B] -> exists u v q, [/\ u \in A, v \in B, path e u (rcons q v), subseq (u:: rcons q v) (x:: rcons p y) & [disjoint q & [predU A & B]]].
proof: Proof. have [m Hm] := ubnP (size p); elim: m x y p Hm => // n IH x y p p_n xA xB pth_p disAB. case: (boolP [disjoint p & [predU A & B]]) => [?|]; first by exists x; exists y; exists p. case/pred0Pn => z /andP[z_in_p z_in_AB]. case/splitP def_p : p _ _ / z_in_p pth_p p_n => [p1 p2]. rewrite rcons_cat cat_path last_rcons => /andP [pth_p1 pth_p2]. rewrite size_cat size_rcons addSn ltnS => size_p. have {z_in_AB} [z_in_A|z_in_B] := orP z_in_AB. - case:(IH z y p2) => //. apply: leq_ltn_trans size_p. exact: leq_addl. move => u [v] [q] [uA vB Q1 Q2 Q3]; exists u; exists v; exists q. split => //. apply: subseq_trans Q2 _. rewrite -(cats1 _ z) -catA cat1s -cat_cons. exact: suffix_subseq. - case:(IH x z p1) => //. apply: leq_ltn_trans size_p. exact: leq_addr. move => u [v] [q] [uA vB Q1 Q2 Q3]; exists u; exists v; exists q. split => //. apply: subseq_trans Q2 _. exact: prefix_subseq. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) fourcolor(hypermap geometry jordan color coloring combinatorial4ct) GraphTheory(hmap_ops)