proposition: Lemma prodv_Fadjoinl (F0 : fieldType) (L : fieldExtType F0) (K F : {subfield L}) (x : L) : (<<K; x>> * F)%VS = <<K * F; x>>%VS.
proof: Proof. apply/eqP; rewrite eqEsubv; apply/andP; split. apply/prodvP => y z /Fadjoin_polyP[p pK ->] zF. have -> : p.[x] * z = (z *: p).[x] by rewrite hornerZ mulrC. rewrite mempx_Fadjoin// polyOverZ//=. by apply/subvP: zF; rewrite field_subvMl. by move: pK; apply/polyOverS/subvP; rewrite field_subvMr. apply/subvP => y /Fadjoin_polyP [p /polyOverP pKF ->]. rewrite horner_coef rpred_sum// => i _. have /memv_mulP[n [us [vs [/allP/= usP /allP/= vsP ->]]]] := pKF i. rewrite mulr_suml rpred_sum // => j _. rewrite mulrAC memv_mul ?rpredM ?rpredX ?memv_adjoin ?vsP ?mem_tnth//. by rewrite subvP_adjoin// usP ?mem_tnth. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)