proposition: Fact n_act_is_action : is_action setT n_act.
proof: Proof. by apply: is_total_action => [t|t a b]; apply: eq_from_tnth => i; rewrite !tnth_map ?act1 ?actM. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat) mathcomp(div seq fintype tuple finset) mathcomp(fingroup action gseries)