proposition: Lemma small_clique (S : {set G}) : #|S| <= 1 -> clique S.
proof: Proof. move/card_le1_eqP => H x y xS yS. by rewrite (H x y) ?eqxx. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)