proposition: Lemma omega_cut H S : {in maxcliques H, forall K, S :&: K != set0} -> ω(H :\: S) < ω(H).
proof: Proof. move/forall_inP; rewrite ltnNge; apply: contraTN; rewrite negb_forall_in. have [/= K maxK geH] := omegaP (H :\: S). move: maxK; rewrite inE => /andP[clK cardK]. apply/exists_inP; exists K; first by rewrite inE geH (cliquesD clK). by move: clK; rewrite !inE subsetD negbK setI_eq0 disjoint_sym -andbA => /and3P[_ -> _]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)