proposition: Lemma maxclique_disjoint K H A : K \in maxcliques H -> [disjoint K & A] -> K \in maxcliques (H :\: A).
proof: Proof. rewrite !inE -!andbA subsetD => /and3P[-> -> maxK] -> /=. apply: leq_trans (sub_omega _) maxK. exact: subsetDl. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)