proposition: Lemma clique2 (x y : G) : x -- y -> clique [set x;y].
proof: Proof. move => xy z z'. rewrite !inE. do 2 case/orP => /eqP-> // ; try by rewrite eqxx. by rewrite sg_sym. Qed.
imports: Coq(Setoid CMorphisms) mathcomp(all_ssreflect) GraphTheory(edone preliminaries bij digraph)