proposition: Lemma stab_iporbits_map_inj P : injective (stab_iporbits_map P).
proof: Proof. Proof using. apply (can_inj (g := stab_iporbits_map P^-1)) => X /=. rewrite /stab_iporbits_map cymapK //= {X} => C HC. rewrite groupV /= -/(stab_iporbits s). by case: (boolP (P \in _)) => [| HP]; rewrite ?perm1 ?permK. 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