proposition: Lemma clique_compl A : cliqueb (A : {set compl G}) = stable A.
proof: Proof. apply/cliqueP/stableP => [clA|stabA] x y xA yA; last move=> xDy. have [<-|xDy] := eqVneq x y; first by rewrite sgP. by move:(clA _ _ xA yA xDy); rewrite {1}/edge_rel/= xDy. by move: (stabA _ _ xA yA); rewrite {2}/edge_rel/= xDy. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)