proposition: Lemma clique_bound K A : K \in cliques A -> #|K| <= ω(A).
proof: Proof. by move => clK; apply: bigmax_sup (leqnn _); rewrite setE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)