proposition: Lemma card_qfpoly : #|{poly %/ h with hI}| = #|R| ^ (size h).-1.
proof: Proof. by rewrite card_monic_qpoly ?hI. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice fintype tuple) mathcomp(div bigop binomial finset finfun ssralg countalg finalg) mathcomp(poly polydiv qpoly perm fingroup falgebra fieldext finfield galois) mathcomp(finalg zmodp matrix vector)