proposition: Lemma sub_perfect A B : A \subset B -> perfect B -> perfect A.
proof: Proof. move=> subAB /forall_inP perfB; apply/forall_inP => C subCA. apply: perfB. exact: subset_trans _ subAB. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)