proposition: Lemma maxclique_clique K H : K \in maxcliques H -> clique K.
proof: Proof. by rewrite !inE -andbA => /and3P[_ /cliqueP ? _]. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)