proposition: Lemma sub_omega A B : A \subset B -> ω(A) <= ω(B).
proof: Proof. move=> subAB; have [K] := omegaP A; rewrite inE => /andP[clA _]. exact/clique_bound/(cliquesW subAB). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)