proposition: Lemma isubgraph_perfect (F G : sgraph) : F ⇀ G -> perfect G -> perfect F.
proof: Proof. by move=> i; rewrite -!perfectT (perfect_imset i); apply: sub_perfect. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring) mathcomp(ssrint)