proposition: Lemma maxstabsets_compl (G : sgraph) (H : {set G}) : maxstabsets (H : {set compl G}) = maxcliques H.
proof: Proof. Abort. Lemma alpha_compl (G : sgraph) (A : {set G}) : α(A : {set compl G}) = ω(A). Abort. Section Induced. Variables (G : sgraph) (H : {set G}). Let i := induced_isubgraph H. Lemma alpha_induced : α(induced H) = α(H). Proof. by rewrite -alphaT (alpha_isubgraph i) imset_valT setE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)