proposition: Lemma qpoly_mulVz (p : {poly %/ h}) : coprimep hQ p -> (qpoly_inv p * p = 1)%R.
proof: Proof. have hQM := monic_mk_monic h. move=> hCp; apply: val_inj; rewrite /qpoly_inv /in_qpoly hCp /=. have p_neq0 : p != 0%R. apply/eqP=> pZ; move: hCp; rewrite pZ. rewrite coprimep0 -size_poly_eq1. by case: size (size_mk_monic_gt1 h) => [|[]]. have F : (egcdp hQ p).1 * hQ + (egcdp hQ p).2 * p %= 1. apply: eqp_trans _ (_ : gcdp hQ p %= _). rewrite eqp_sym. by case: (egcdpP (mk_monic_neq0 h) p_neq0). by rewrite -size_poly_eq1. rewrite rmodp_mulml // -scalerAl rmodpZ // rmodp_mulml //. rewrite -[rmodp]/Pdiv.Ring.rmodp -!Pdiv.IdomainMonic.modpE //. have := eqp_modpl hQ F. rewrite modpD // modp_mull add0r // . rewrite [(1 %% _)%R]modp_small => // [egcdE|]; last first. by rewrite size_polyC oner_eq0 size_mk_monic_gt1. rewrite {2}(eqpfP egcdE) lead_coefC divr1 alg_polyC scale_polyC mulVf //. rewrite lead_coef_eq0. apply/eqP => egcdZ. by move: egcdE; rewrite -size_poly_eq1 egcdZ size_polyC eq_sym eqxx. 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)