proposition: Lemma isubgraph_cliques (B K : {set F}) : (K \in cliques B) = (i @: K \in cliques (i @: B)).
proof: Proof. by rewrite !inE inj_imsetS // -cliqueb_isubgraph. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)