proposition: Lemma sub_clique K K' : K' \subset K -> clique K -> clique K'.
proof: Proof. by move=> /subsetP subK clK x y /subK xK /subK yK; exact: clK. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)