proposition: Lemma edivpP m d : edivp_spec m d (edivp m d) (lead_coef d \in GRing.unit).
proof: Proof. have hC : GRing.comm d (lead_coef d)%:P by rewrite /GRing.comm mulrC. case ud: (lead_coef d \in GRing.unit); last first. rewrite edivp_redivp // redivp_def; constructor; rewrite ?ltn_rmodp // ?ud //. by rewrite rdivp_eq. have cdn0: lead_coef d != 0 by apply: contraTneq ud => ->; rewrite unitr0. rewrite unlock ud redivp_def; constructor => //. rewrite -scalerAl -scalerDr -mul_polyC. have hn0 : (lead_coef d ^+ rscalp m d)%:P != 0. by rewrite polyC_eq0; apply: expf_neq0. apply: (mulfI hn0); rewrite !mulrA -exprVn !polyC_exp -exprMn -polyCM. by rewrite divrr // expr1n mul1r -polyC_exp mul_polyC rdivp_eq. move=> dn0; rewrite size_scale ?ltn_rmodp // -exprVn expf_eq0 negb_and. by rewrite invr_eq0 cdn0 orbT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)