proposition: Lemma separator_from_smerge2 (G : sgraph) (x y : G) (xDy : x != y) (x' := Sub x xDy) (S : {set smerge2 G x y}) : vseparator S -> x' \notin S -> vseparator (val @: S).
proof: Proof. move=> /vseparator_separation [V1 [V2 [psepV def_S]]] xNS. wlog x_V1 : V1 V2 psepV def_S / x' \notin V2 => [W|]. { case: (boolP (x' \in V2)) => [x_V2|]; last exact: (W V1 V2). apply: (W V2 V1); rewrite 1?proper_separation_symmetry 1?setIC //. case: psepV => sepV _. apply: contraNN xNS => x_V1. by rewrite def_S inE x_V1 x_V2. } suff: proper_separation (y |: val @: V1) (val @: V2). { move/proper_vseparator. suff -> : (y |: val @: V1) :&: (val @: V2) = val @: S by []. apply/setP => u; rewrite def_S inE imsetI ?inE; last exact: (in2W val_inj). rewrite (@andb_id2r _ _ (u \in val @: V1)) // => /imsetP [u0 _ ->]. by rewrite (negbTE (valP u0)). } split; first split. - move => u. case: (eqVneq u y) => [->|uDy]; rewrite !inE ?eqxx ?(negbTE uDy) //=. case: psepV => sepV _. have := sepV.1 (Sub u uDy). by rewrite Sub_imset imsetU inE. - move => u v; rewrite !inE negb_or => u_V1 /andP [vDy v_V2]. case: psepV => sepV _. have v'_V2 : (Sub v vDy) \notin V1. { by apply: contraNN v_V2 => H; apply/imsetP; exists (Sub v vDy). } have vDx : v != x. { apply: contraNneq x_V1 => ?; subst v. apply: sep_inR sepV _. by rewrite /x' (bool_irrelevance xDy vDy). } case: (eqVneq u y) => [?|uDy]; first subst u. + apply: contraFF (sepV.2 _ _ x_V1 v'_V2) => yv. by rewrite /edge_rel/= eqxx vDx [v -- y]sgP yv orbT. + have u'_V1 : (Sub u uDy) \notin V2. { by apply: contraNN u_V1 => H; apply/imsetP; exists (Sub u uDy). } apply: contraFF (sepV.2 _ _ u'_V1 v'_V2) => uv. rewrite /edge_rel/=. rewrite (negbTE vDx) /= andbT. by case: (eqVneq u x) => [<-|//]; rewrite [v -- u]sgP uv. - case: psepV => _ [u [v [u_V1 v_V2]]]. exists (val u),(val v). by rewrite !(inE,mem_imset) // negb_or (valP v). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity minor treewidth arc set_tac)