proposition: Lemma subgraph_K4_free (G H : sgraph) : subgraph H G -> K4_free G -> K4_free H.
proof: Proof. move/sub_minor. exact: minor_K4_free. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)