proposition: Lemma scaleD (p q : {poly R}) u : (p + q) \shift u = p \shift u + (q \shift u).
proof: Proof. by rewrite /scaleX_poly linearD. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc