proposition: Lemma cons_polyK : forall p : {poly R}, cons_poly p.[0] (\poly_(i < (size p).-1) p`_i.+1) = p.
proof: Proof. move=> p; rewrite cons_poly_def addrC -[X in _ = X]coefK. case sz : (size p) => [ | s]. move/eqP: sz; rewrite size_poly_eq0 => /eqP => sz. by rewrite sz horner0 polyC0 add0r /= polyseq0 !polyd0 mul0r. rewrite [s.+1.-1]/= !poly_def big_ord_recl; congr (_ + _). by rewrite expr0 alg_polyC horner_coef0. rewrite big_distrl; apply: eq_bigr; move=> [i ci] _ /=. by rewrite -scalerAl /bump leq0n add1n exprS mulrC. 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