proposition: Lemma minor_K4_free (G H : sgraph) : minor G H -> K4_free G -> K4_free H.
proof: Proof. move => M F C. apply: F. exact: minor_trans C. Qed.
imports: Coq(RelationClasses) mathcomp(all_ssreflect) GraphTheory(edone preliminaries digraph) GraphTheory(sgraph treewidth set_tac)