proposition: Lemma non_forerst_K3 (G : sgraph) : ~ is_forest [set: G] -> minor G 'K_3.
proof: Proof. move/is_forestP/is_forestPn => [x0] [y0] [p0] [q0] [_ _ pDq]. have [x [y] [p1] [p2] [p12_disj p1_ne]] := disjoint_part (valP p0) (valP q0) pDq. clear x0 y0 p0 q0 pDq. pose phi (i : 'K_3) : {set G} := match i with | Ordinal 0 _ => [set x] | Ordinal 1 _ => interior p1 | Ordinal 2 _ => y |: interior p2 | Ordinal _ _ => set0 end. suff: minor_rmap phi by apply: minor_of_rmap. have xDy : x != y. { apply: contra_neq p1_ne => ?; subst y. by rewrite /path_of_ipath (irredxx (valP p1)) interior_idp. } apply: ordered_rmap; first exact: ord_inj; split. - case => [[|[|[|i]]] Hi] //=; [exact: set10 | exact: setU1_neq]. - case => [[|[|[|i]]] Hi] //=. + exact: connected1. + exact: connected_interior. + exact: connected_interiorR. - case => [[|[|[|i]]] Hi]; case => [[|[|[|j]]] Hj] //= _ _. + by rewrite disjoints1 !inE eqxx. + by rewrite disjoints1 !inE eqxx (negbTE xDy). + rewrite disjoint_sym disjointsU // ?disjoints1 1?disjoint_sym //. by rewrite !inE eqxx. - case => [[|[|[|i]]] Hi]; case => [[|[|[|j]]] Hj] //= _ _. + apply: path_neighborL => //. by rewrite inE. + exact: neighbor_interiorL. + apply: neighborUl. rewrite neighborC. apply: path_neighborR => //. by rewrite inE. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)