proposition: Lemma divpE p q : p %/ q = (lead_coef q)^-(rscalp p q) *: (rdivp p q).
proof: Proof. have [-> | qn0] := eqVneq q 0; first by rewrite rdivp0 divp0 scaler0. by rewrite Idomain.divpE unitfE lead_coef_eq0 qn0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)