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