proposition: Lemma alg_polyOver E p : map_poly (in_alg L) p \is a polyOver E.
proof: Proof. by apply/(polyOverS (subvP (sub1v _)))/polyOver1P; exists p. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq div) mathcomp(choice fintype tuple finfun bigop ssralg countalg) mathcomp(finalg zmodp matrix vector falgebra poly polydiv) mathcomp(mxpoly generic_quotient)