proposition: Lemma gal_AEnd x : gal_repr x \in kAEnd 1 (agenv V).
proof: Proof. rewrite /gal_repr; case/gal_sgval: x => _ /=/morphimP[g Ng autEg ->]. rewrite val_coset //=; case: repr_rcosetP => f; rewrite groupMr // !inE kAut1E. by rewrite kAutE -andbA => /and3P[_ /fixedSpace_limg-> _]. 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)