proposition: Lemma act_f_1 : forall k, act_f k 1 = k.
proof: Proof. by move=> k; apply/ffunP=> a; rewrite ffunE invg1 permE. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop finset fingroup) mathcomp(action perm primitive_action)