proposition: Lemma coprimep_unit (p : {poly %/ h}) : p != 0%R -> coprimep hQ p.
proof: Proof. move=> pNZ. rewrite irreducible_poly_coprime //; last first. by case: hI; rewrite mk_monicE. apply: contra pNZ => H; case: eqP => // /eqP /dvdp_leq /(_ H). by rewrite leqNgt size_mk_monic. 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)