proposition: Lemma stable_isubgraph (S : {set F}) : stable S = stable (i @: S).
proof: Proof. rewrite !stableEedge (@forall2_imset _ _ i i). apply: eq_forall_in => x xS; apply: eq_forall_in => y yS. by rewrite isubgraph_mono. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)