proposition: Lemma no_K4_smallest_vseparator (G : sgraph) : ~ minor G K4 -> #|G| <= 3 \/ (exists S : {set G}, smallest vseparator S /\ #|S| <= 2).
proof: Proof. move => HM. case (boolP (3 < #|G|)) => sizeG; last by rewrite leqNgt; left. right. case: (boolP ([exists (S : {set G} | #|S| <= 2), vseparatorb S])). - case/exists_inP => /= S sizeS sepS. case: (arg_minnP (fun a : {set G} => #|a|) sepS) => U /vseparatorP sepU HU. exists U. repeat split => //. + move => V /vseparatorP. exact: HU. + move: (HU S sepS) => ?. exact: leq_trans sizeS. - move/exists_inPn => H. exfalso. apply HM. apply K4_of_vseparators => //. move => S. move: (H S). rewrite unfold_in (rwP (vseparatorP _)) => H'. apply: contraTT. by rewrite ltnNge negbK. Qed.
imports: Coq(Setoid Morphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries set_tac digraph) GraphTheory(sgraph treewidth minor connectivity)