proposition: Lemma cliqueU1 x K : K \subset N(x) -> clique K -> clique (x |: K).
proof: Proof. move => /subsetP subKNx clK u v /setU1P[-> {u}|uK] /setU1P[-> {v}|vK]. - by rewrite eqxx. - by move/subKNx : vK; rewrite inE. - by move/subKNx : uK; rewrite inE sgP. - exact: clK. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)