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