proposition: Lemma omega_compl (G : sgraph) (A : {set G}) : ω(A : {set compl G}) = α(A).
proof: Proof. case: omegaP => K. rewrite maxcliques_compl. exact: (@card_maxstabset G). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)