proposition: Lemma kAEnd_group_set K E : group_set (kAEnd K E).
proof: Proof. apply/group_setP; split=> [|f g]; first by rewrite inE /kAut kHom1 lim1g eqxx. rewrite !inE !kAutE => /andP[homKf EfE] /andP[/(kHomSr EfE)homKg EgE]. by rewrite (comp_kHom_img homKg homKf) limg_comp (subv_trans _ EgE) ?limgS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg poly) mathcomp(polydiv finset fingroup morphism quotient perm) mathcomp(action zmodp cyclic matrix mxalgebra vector) mathcomp(falgebra fieldext separable)