proposition: Lemma qpolyC_proof k : (k%:P : {poly R}) \is a poly_of_size (size (mk_monic h)).-1.
proof: Proof. rewrite qualifE/= -ltnS size_polyC prednK ?size_mk_monic_gt0 //. by rewrite (leq_ltn_trans _ size_mk_monic_gt1) //; case: eqP. 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)