proposition: Lemma forest_vseparator (G : sgraph) : is_forest [set: G] -> 3 <= #|G| -> exists2 S : {set G}, vseparator S & #|S| <= 1.
proof: Proof. move => forest_G card_G. have {card_G} [x [y [xDy xy]]] := forest3 forest_G card_G. have [/connect_irredP [p Ip]|nCxy]:= (boolP (connect sedge x y)). move/forestT_unique in forest_G. - have/set0Pn [z z_p] : interior p != set0. { apply: contraNneq xy => Ip0. by case: (interior0E xDy Ip Ip0). } exists [set z]; last by rewrite cards1. exists x; exists y; apply: separatesI. move: (interiorN z_p); rewrite !inE negb_or ![z == _]eq_sym => /andP[-> ->]. split => // q Iq. exists z; rewrite ?inE ?eqxx //. apply: interiorW. by rewrite (forest_G _ _ _ _ Iq Ip). - exists set0; last by rewrite cards0. exists x;exists y. split; rewrite ?inE // => p. case: notF. apply: contraNT nCxy => _. exact: Path_connect p. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph sgraph) GraphTheory(connectivity set_tac)