proposition: Lemma cliques_subset (A K : {set G}) : K \in cliques A -> K \subset A.
proof: Proof. by rewrite !inE => /andP[-> _]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)