proposition: Lemma CP_base U x y : x \in CP U -> y \in CP U -> exists x' y':G, [/\ x' \in U, y' \in U & [set x;y] \subset cp x' y'].
proof: Proof. Proof using. move => U1 U2. case/bigcupP : U1 => [[x1 x2]]. case/bigcupP : U2 => [[y1 y2]] /=. rewrite !inE /= => /andP[Uy1 Uy2] cp_y /andP[Ux1 Ux2] cp_x. case: (boolP (x \in cp y1 y2)) => [C|Wx]; first by exists y1; exists y2; rewrite subUset !sub1set C. case: (boolP (y \in cp x1 x2)) => [C|Wy]; first by exists x1; exists x2; rewrite subUset !sub1set C. gen have H,A: x x1 x2 y1 y2 {Ux1 Ux2 Uy1 Uy2 Wy cp_y} Wx cp_x / (x \in cp x1 y1) || (x \in cp x2 y2). { case/cpPn : Wx => p irr_p av_x. apply: contraTT cp_x. rewrite negb_or => /andP[/cpPn [s s1 s2] /cpPn [t t1 t2]]. apply (cpNI (p := pcat s (pcat p (prev t)))). by rewrite !mem_pcat !mem_prev (negbTE av_x) (negbTE s2) (negbTE t2). } have {H} B : (y \in cp x1 y1) || (y \in cp x2 y2). { rewrite -(cp_sym y1 x1) -(cp_sym y2 x2). exact: H. } wlog {A} /andP [Hx Hy] : x1 x2 y1 y2 A B cp_x cp_y Ux1 Ux2 Uy1 Uy2 Wx Wy / (x \in cp x1 y1) && (y \notin cp x1 y1). { case: (boolP (y \in cp x1 y1)) A B => A; case: (boolP (x \in cp x1 y1)) => /= B C D W. - by exists x1; exists y1; rewrite subUset !sub1set B. - case: (boolP (y \in cp x2 y2)) => E. + exists x2; exists y2; by rewrite subUset !sub1set C. + move: (W x2 x1 y2 y1). rewrite (cp_sym x2 x1) (cp_sym y2 y1) A C /= orbT. exact. - apply: (W x1 x2 y1 y2) => //. by rewrite B. by rewrite D. - exists x2; exists y2; by rewrite subUset !sub1set C D. } rewrite (negbTE Hy) /= in B. case: (boolP (x \in cp x2 y2)) => [C|Wx']; first by exists x2; exists y2; rewrite subUset !sub1set C. exists x1. exists y2. rewrite subUset !sub1set. split => //. apply/andP; split. - apply: contraTT cp_x => C. apply: cpN_trans C _. by rewrite cp_sym. - apply: contraTT cp_y. apply: cpN_trans. by rewrite cp_sym. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph connectivity)