proposition: Lemma divpp p : p != 0 -> p %/ p = (lead_coef p ^+ scalp p p)%:P.
proof: Proof. move=> np0; have := divp_eq p p. suff -> : p %% p = 0 by rewrite addr0 -mul_polyC; move/(mulIf np0). rewrite modpE Ring.rmodpp; last by red; rewrite mulrC. by rewrite scaler0 if_same. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)