proposition: Lemma Sym_group_set : group_set Sym.
proof: Proof. apply/group_setP; split => [|s t] /[!inE]; [exact: perm_on1 | exact: perm_onM]. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(choice fintype tuple finfun bigop finset binomial) mathcomp(fingroup morphism)