proposition: Lemma alpha_isubgraph (F G : sgraph) (i : F ⇀ G) (A : {set F}) : α(A) = α(i @: A).
proof: Proof. by rewrite -omega_compl (omega_isubgraph (isubgraph_compl i)) omega_compl. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)