proposition: Lemma maxclique_opn H K v : v \in H -> K \in maxcliques H -> K \subset N(v) -> v \in K.
proof: Proof. rewrite !inE -andbA => vH /and3P[subKH /cliqueP clK maxK] subNvK. have/cliqueP clvK : clique (v |: K) by apply: cliqueU1. apply: contraTT maxK => vNK ; rewrite -ltnNge. rewrite -add1n -[1 + _]/(true + #|K|) -vNK -cardsU1; apply: clique_bound. by rewrite !inE clvK subUset sub1set vH subKH. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)