proposition: Lemma setact1 x a : to^* [set x] a = [set to x a].
proof: Proof. Proof using. by rewrite /setact imset_set1. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype div) mathcomp(finset fingroup perm morphism action)