proposition: Lemma poly_of_size_mod p : rmodp p (mk_monic h) \is a poly_of_size (size (mk_monic h)).-1.
proof: Proof. rewrite qualifE/= -ltnS prednK ?size_mk_monic_gt0 //. by apply: ltn_rmodpN0; rewrite mk_monic_neq0. 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)