proposition: Lemma chi_isubgraph (A : {set F}) : χ(A) = χ(i @: A).
proof: Proof. apply/eqP; rewrite eqn_leq; apply/andP; split. - case: (chiP (i @: A)) => P /preim_coloring colP minP. exact: leq_trans (color_bound colP) (leq_imset_card _ _). - case: (chiP A) => P colP minP. rewrite coloring_isubgraph in colP; apply: leq_trans (color_bound colP) _. by rewrite card_imset //; apply/imset_inj/isubgraph_inj. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)