proposition: Lemma clique_to_isubgraph (K A : {set G}) : K \in cliques A -> i @^-1: K \in cliques (i @^-1: A).
proof: Proof. rewrite !inE => /andP[subKA /cliqueP clK]. rewrite preimsetS //= cliqueb_isubgraph; apply/cliqueP. by apply: sub_clique clK; rewrite sub_imset_pre preimsetS. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)