proposition: Lemma mk_monic_X (R : ringType) : mk_monic 'X = 'X :> {poly R}.
proof: Proof. by rewrite /mk_monic size_polyX monicX. 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)