proposition: Theorem TW1_forest G : (exists T B, sdecomp T G B /\ width B <= 2) <-> is_forest [set: G].
proof: Proof. split => [[T] [B] [decB wB]|]; last exact: forest_TW1. apply/K3_free_forest. exact: treewidth_K_free decB wB. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)