proposition: Lemma omegaP A : omega_spec A ω(A).
proof: Proof. rewrite /omega_mem setE. have [/= K clK maxK] := eq_bigmax_cond (fun A => #|A|) (cliques_gt0 A). by rewrite maxK; apply: OmegaSpec; rewrite inE clK -maxK -{2}[A]setE leqnn. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)