proposition: Lemma monic_mk_monic : (mk_monic h) \is monic.
proof: Proof. rewrite /mk_monic; case: leqP=> [_|/=]; first by apply: monicX. by case E : (h \is monic) => [->//|] => _; apply: 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)