proposition: Lemma chiD1 H S : stable S -> χ(H) <= χ(H :\: S).+1.
proof: Proof. move=> stabS; wlog subSH : S stabS / S \subset H. move => /(_ (S :&: H)); rewrite setDIr setDv setU0 subsetIr; apply => //. by apply: sub_stable stabS; rewrite subsetIl. have [->|SD0] := eqVneq S set0; first by rewrite setD0. case: (chiP (H :\: S)) => P colP _; have := coloringU1 stabS SD0 colP. rewrite disjoint_sym disjoints_subset subsetDr [S :|: _]setUC setDK // => /(_ isT) => colP'. by apply: leq_trans (color_bound colP') _; rewrite cardsU1; case (_ \in _). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)