proposition: Lemma divp_eq p q : (lead_coef q ^+ scalp p q) *: p = (p %/ q) * q + (p %% q).
proof: Proof. rewrite divpE modpE scalpE. case uq: (lead_coef q \in GRing.unit); last by rewrite rdivp_eq. rewrite expr0 scale1r; have [->|qn0] := eqVneq q 0. by rewrite lead_coef0 expr0n /rscalp unlock eqxx invr1 !scale1r rmodp0 !simp. by rewrite -scalerAl -scalerDr -rdivp_eq scalerA mulVr (scale1r, unitrX). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)