proposition: Lemma joingU1 (gt : finGroupType) (a : gt) (S : {set gt}) : <[a]> <*> <<S>> = << a |: S >>.
proof: Proof. by rewrite joing_idr joing_idl joingE. Qed.
imports: HB(structures) mathcomp(all_ssreflect) mathcomp(fingroup perm morphism presentation) mathcomp(ssralg poly ssrint) permcomp tools permuted combclass congr