proposition: Lemma maxcliques_compl (G : sgraph) (H : {set G}) : maxcliques (H : {set compl G}) = maxstabsets H.
proof: Proof. apply/setP => A. rewrite !inE clique_compl; apply: andb_id2l => /andP[subAH stabA]. rewrite /omega_mem /alpha_mem setE /=. by under eq_bigl => B do rewrite inE clique_compl -(@in_stabsets G). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)