proposition: Lemma omega_eq0 A : (ω(A) == 0) = (A == set0).
proof: Proof. apply/idP/idP => [|/eqP->]; last by rewrite omega0. apply: contraTT => /set0Pn[x xH]; rewrite -lt0n -(cards1 x). apply: clique_bound. rewrite inE sub1set xH. exact/cliqueP/clique1. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)