proposition: Lemma omega_induced : ω(induced H) = ω(H).
proof: Proof. by rewrite -omegaT (omega_isubgraph i) imset_valT setE. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)