proposition: Lemma setact0 a : to^* set0 a = set0.
proof: Proof. Proof using. by rewrite /setact imset0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype div) mathcomp(finset fingroup perm morphism action)