proposition: Lemma mulpK p q : q != 0 -> p * q %/ q = lead_coef q ^+ scalp (p * q) q *: p.
proof: Proof. move=> qn0; apply: (rregP qn0); rewrite -scalerAl divp_eq. suff -> : (p * q) %% q = 0 by rewrite addr0. rewrite modpE RingComRreg.rmodp_mull ?scaler0 ?if_same //. by red; rewrite mulrC. by apply/rregP; rewrite lead_coef_eq0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)