proposition: Lemma primitive_poly_in_qpoly_eq0 p : (in_qpoly h p == 0) = (h %| p).
proof: Proof. have hM : h \is monic by case/and4P:Hh. have hMi : monic_irreducible_poly h by apply: primitive_mi. apply/eqP/idP => [/val_eqP /= | hDp]. by rewrite -Pdiv.IdomainMonic.modpE mk_monicE. by apply/val_eqP; rewrite /= -Pdiv.IdomainMonic.modpE mk_monicE. 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)