proposition: Lemma maxstabset_to_induced (G : sgraph) (H : {set G}) (S : {set G}) : S \in maxstabsets H -> val @^-1: S \in maxstabsets [set: induced H].
proof: Proof. pose i := induced_isubgraph H. rewrite !inE subsetT (stable_isubgraph i) -andbA /= => /and3P[S1 S2 S3]. have subSi : S \subset codom i. { apply: subset_trans S1 _; apply/subsetP => x xH. by apply/codomP; exists (Sub x xH). } rewrite (@can_preimset _ _ i) ?S2 //= (@inj_card_preimset _ _ i) //=. rewrite alphaT alpha_induced //. exact: val_inj. Qed.
imports: mathcomp(all_ssreflect) GraphTheory(preliminaries bij digraph) GraphTheory(sgraph dom partition)