proposition: Lemma connectedI_clique (G : sgraph) (A B S : {set G}) : connected A -> clique S -> (forall x y (p : Path x y), p \subset A -> x \in B -> y \notin B -> exists2 z, z \in p & z \in S :&: B) -> connected (A :&: B).
proof: Proof. move => conA clS H x y /setIP [X1 X2] /setIP [Y1 Y2]. case: (altP (x =P y)) => [->|xDy]; first exact: connect0. case/connect_irredRP : (conA _ _ X1 Y1) => // p Ip subA. case: (boolP (p \subset B)) => subB. - apply connectRI with p => z zp. by set_tac. - case/subsetPn : subB => z Z1 Z2. gen have C,Cx : x y p Ip subA X1 X2 Y1 Y2 Z1 Z2 {xDy} / exists2 s, s \in S :&: A :&: B & connect (restrict (A :&: B) sedge) x s. { case: (split_at_first (A := [predC B]) Z2 Z1) => u' [p1] [p2] [P1 P2 P3]. subst p. case/irred_catE : Ip => Ip1 Ip2 Ip. case/splitR : (p1); first by apply: contraNneq P2 => <-. move => u [p1'] [uu'] E. subst p1. have uB : u \in B. apply: contraTT (uu') => C. by rewrite [u]P3 ?sgP // !inE. exists u. case: (H _ _ (edgep uu')) => //. - apply: subset_trans subA. apply: subset_trans (subset_pcatL _ _). exact: subset_pcatR. - move => ?. rewrite !inE mem_edgep. case/orP => /eqP-> /andP[U1 U2]. + by rewrite U1 U2 (subsetP subA) // !inE. + by rewrite !inE U2 in P2. - apply connectRI with p1' => v Hv. rewrite !inE (subsetP subA) ?inE ?Hv //=. move: Ip1. rewrite irred_edgeR andbC => /andP [Ip1]. apply: contraNT => C. by rewrite -(P3 v) // !inE Hv. } case: Cx => s. rewrite !inE -andbA => /and3P [S1 S2 S3 S4]. case: (C _ _ (prev p)); rewrite ?mem_prev ?irred_rev //. + apply: subset_trans subA. apply/subsetP => ?. by rewrite !inE. + move => t. rewrite !inE -andbA => /and3P [T1 T2 T3 T4]. apply: connect_trans S4 _. rewrite srestrict_sym. apply: connect_trans T4 _. case: (altP (t =P s)) => [-> //|E]. apply: connect1 => /=. by rewrite !inE clS. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries set_tac digraph) GraphTheory(sgraph treewidth minor connectivity)