proposition: Lemma in_qpoly_small (p : {poly R}) : size p < size (mk_monic h) -> in_qpoly p = p :> {poly R}.
proof: Proof. exact: rmodp_small. 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)