proposition: Lemma cliqueP S : reflect (clique S) (cliqueb S).
proof: Proof. apply: (equivP forall_inP). setoid_rewrite <- (rwP forall_inP). setoid_rewrite <- (rwP implyP). by firstorder. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)