proposition: Lemma qpolyXE : 2 < size h -> h \is monic -> 'qX = 'X :> {poly R}.
proof: Proof. move=> sh_gt2 h_mo. by rewrite in_qpoly_small // size_polyX /mk_monic ifT // (ltn_trans _ sh_gt2). 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)