proposition: Lemma rdvdp_eq q p : rdvdp q p = (lead_coef q ^+ rscalp p q *: p == rdivp p q * q).
proof: Proof. rewrite rdivp_eq; apply/rmodp_eq0P/eqP => [->|/eqP]; first by rewrite addr0. by rewrite eq_sym addrC -subr_eq subrr; move/eqP<-. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop ssralg poly)