proposition: Lemma poly_of_qpolyX (p : {poly %/ h}) n : p ^+ n = rmodp ((p : {poly A}) ^+ n) (mk_monic h) :> {poly A}.
proof: Proof. have HhQ := monic_mk_monic h. elim: n => //= [|n IH]. rewrite rmodp_small // size_polyC ?(leq_ltn_trans _ (size_mk_monic_gt1 _)) //. by case: eqP. by rewrite exprS /= IH // rmodp_mulmr // -exprS. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(bigop binomial finset finfun ssralg countalg finalg poly polydiv) mathcomp(perm fingroup matrix mxalgebra mxpoly vector countalg)