proposition: Lemma n_act0 (t : 0.-tuple sT) a : n_act to t a = [tuple].
proof: Proof. exact: tuple0. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(div seq fintype tuple finset) mathcomp(fingroup action gseries)