proposition: Lemma foo (T : finType) (s : seq T) (A : {set T}) : 1 < #|A| -> {subset A <= s} -> exists x y s1 s2 s3, [/\ x \in A, y \in A, x != y, s = s1 ++ x :: s2 ++ y :: s3 & [disjoint A & s2]].
proof: Proof. move=> lt1A; elim/(size_ind (@size T)) : s => s IH subAs. have hasAs : has (mem A) s. { case/card_gt0P : (ltnW lt1A) => x xA; apply/hasP; exists x => //. exact: subAs. } case/split_find def_s : {-}s _ _ / hasAs => [/= x s1 s2 xA nAs1]. have hasAs2 : has (mem A) s2. { apply: contraTT lt1A => nAs2; rewrite -leqNgt; apply/card_le1_eqP => u v uA vA. wlog suff eq_x : u uA / u = x; first by rewrite [v]eq_x // [u]eq_x. rewrite -!disjoint_has in nAs1 nAs2. move/subAs : (uA). rewrite def_s !(mem_cat,mem_rcons,inE). by rewrite (disjointFl nAs1) // (disjointFl nAs2) // !orbF => /eqP. } case/split_find def_s2 : {-}s2 _ _ / hasAs2 => [/= y s21 s22 yA nAs21]. rewrite -!disjoint_has in nAs1 nAs21. have [eq_xy|xDy] := eqVneq x y. - subst y; have sub_A_s2 : {subset A <= s2}. { move=> u uA; move/subAs : (uA). rewrite def_s mem_cat mem_rcons inE (disjointFl nAs1) ?orbF //. by case/predU1P => [->|//]; rewrite def_s2 mem_cat mem_rcons mem_head. } have size_s2 : size s2 < size s. { by rewrite def_s size_cat size_rcons addSn ltnS leq_addl. } have [u[v[p1[p2[p3[uA vA uDv def_s2' disAp2]]]]]] := IH s2 size_s2 sub_A_s2. by exists u,v,(rcons s1 x ++ p1),p2,p3; split; rewrite // def_s def_s2' /= -catA. - exists x,y,s1,s21,s22; rewrite disjoint_sym nAs21; split => //. by rewrite def_s def_s2 -!cats1 /= -!catA. Qed.
imports: mathcomp(all_ssreflect) fourcolor(hypermap geometry color coloring walkup combinatorial4ct cfmap) GraphTheory(edone preliminaries bij digraph sgraph) GraphTheory(connectivity minor hmap_ops smerge hcycle arc)