proposition: Lemma card_monic_qpoly (R : finRingType) (h : {poly R}): 1 < size h -> h \is monic -> #|{poly %/ h}| = #|R| ^ (size h).-1.
proof: Proof. by move=> sh_gt1 hM; rewrite card_qpoly /mk_monic sh_gt1 hM. 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)