proposition: Lemma perfect_induced H : perfect (induced H) = perfect H.
proof: Proof. pose i := induced_isubgraph H. by rewrite -perfectT (perfect_imset i) /= imset_valT setE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)