proposition: Lemma cliquePn S : reflect (exists x y, [/\ x \in S, y \in S, x != y & ~~ x -- y]) (~~ cliqueb S).
proof: Proof. apply: (equivP forall_inPn). setoid_rewrite <- (rwP forall_inPn). setoid_rewrite negb_imply. setoid_rewrite <- (rwP andP). by firstorder. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)