proposition: Lemma unit_is_groupAction : @is_groupAction _ R setT setT unit_action.
proof: Proof. move=> u _ /[1!inE]; apply/andP; split; first by apply/subsetP=> x /[1!inE]. by apply/morphicP=> x y _ _; rewrite !actpermE /= [_ u]mulrDl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype finset fingroup morphism perm action) mathcomp(ssralg countalg)