proposition: Lemma perfect_imset (F : sgraph) (i : F ⇀ G) (A : {set F}) : perfect A = perfect(i @: A).
proof: Proof. apply/idP/idP. - move/forall_inP => perfIA; apply/forall_inP => B subBA. have subBi : B \subset codom i by apply: subset_trans subBA (imset_codom _ _). rewrite -[B](can_preimset i) // -omega_isubgraph -chi_isubgraph; apply perfIA. rewrite -(@inj_imsetS _ _ i) // ?can_preimset //. exact: isubgraph_inj. - move/forall_inP => perfA; apply/forall_inP => B ?. by rewrite (omega_isubgraph i) (chi_isubgraph i); apply/perfA/imsetS. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph sgraph) GraphTheory(dom partition coloring)