proposition: Lemma rdivpp : rdivp d d = (lead_coef d ^+ rscalp d d)%:P.
proof: Proof. have dn0 : d != 0 by rewrite -lead_coef_eq0 rreg_neq0. move: (rdivp_eq d); rewrite rmodpp addr0. suff ->: GRing.comm d (lead_coef d ^+ rscalp d d)%:P by move/(rreg_lead Rreg)->. by rewrite polyC_exp; apply: commrX. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)