proposition: Lemma galM E (x y : gal_of E) a : a \in E -> (x * y)%g a = y (x a).
proof: Proof. rewrite /= -comp_lfunE; apply/eq_galP; rewrite ?limg_comp ?limg_gal //. by rewrite morphM /= ?gal_reprK ?gal_AEnd. 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)