proposition: Lemma modpE p q : p %% q = (lead_coef q)^-(rscalp p q) *: (rmodp p q).
proof: Proof. have [-> | qn0] := eqVneq q 0. by rewrite rmodp0 modp0 /rscalp unlock eqxx lead_coef0 expr0 invr1 scale1r. by rewrite Idomain.modpE unitfE lead_coef_eq0 qn0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)