proposition: Lemma diso_perfect_induced (G : sgraph) (U V : {set G}) : induced U ≃ induced V -> perfect U -> perfect V.
proof: Proof. move => i; rewrite -perfect_induced -perfectT (diso_perfect i). have -> : i @: [set: induced U] = [set: induced V]. { by apply/setP => x; rewrite !inE -[x](bijK' i) imset_f. } by rewrite perfectT perfect_induced. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)