proposition: Fact gal_is_morphism : {in kAEnd 1 (agenv V) &, {morph gal : x y / x * y}%g}.
proof: Proof. move=> f g /= autEa autEb; congr (Gal _). by rewrite !morphM ?mem_morphim // (subsetP (kAEnd_norm 1 _)). 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)