proposition: Lemma qpoly_intro_unit (p q : {poly %/ h}) : (q * p = 1)%R -> coprimep hQ p.
proof: Proof. have hQM := monic_mk_monic h. case; rewrite -[rmodp]/Pdiv.Ring.rmodp -!Pdiv.IdomainMonic.modpE // => qp1. have:= coprimep1 hQ. rewrite -coprimep_modr -[1%R]qp1 !coprimep_modr coprimepMr; by case/andP. 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)