proposition: Theorem K3_free_forest G : ~ minor G 'K_3 <-> is_forest [set: G].
proof: Proof. split. - rewrite (rwP (is_forestP _)). apply: contra_notT. move/is_forestP. exact: non_forerst_K3. - case/forest_TW1 => T [B []]. exact: treewidth_K_free. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)