proposition: Lemma scal_polyE (p q : {poly R}) : scal_poly (N:=nat) (R:=R) p q = rscalp p q.
proof: Proof. rewrite /scal_poly -[rscalp p q]/((rscalp p q, rdivp p q, rmodp p q).1.1). rewrite -redivp_def div_rec_polyE /redivp /redivp_expanded_def. by rewrite unlock /= /spec_nat /spec_id. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq zmodp) mathcomp(path choice fintype tuple finset ssralg bigop poly polydiv) CoqEAL(param refinements hrel poly_op)