proposition: Lemma stable_induced (K : {set induced H}) : stable K = stable (val @: K).
proof: Proof. exact: (stable_isubgraph i). Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)