proposition: Lemma stab_iporbits_stab P : (if P \in stab_iporbits s then P else 1) @: porbits s \subset porbits s.
proof: Proof. Proof using. case: (boolP (_ \in _)) => [|_]. - by rewrite !inE => /andP[/im_perm_on -> _]. - by rewrite (eq_imset (g := id)) ?imset_id // => x; rewrite perm1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq fintype) mathcomp(tuple path bigop finset div) mathcomp(fingroup perm action gproduct morphism) tools partition permcomp cycles cycletype