proposition: Lemma cliqueD K H : clique K -> clique (K :\: H).
proof: Proof. by move => clK x y /setDP[xK _] /setDP[yK _]; exact: clK. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)