proposition: Lemma poly_cons (p : seqpoly R) (a : R) : \poly_(i < size (a :: p)) (a :: p)`_i = a%:P + (\poly_(i < size p) p`_i) * 'X.
proof: Proof. rewrite !poly_def big_ord_recl big_distrl /= expr0 alg_polyC /bump /=. apply: congr2=> //; apply: eq_bigr=> i _. by rewrite add1n exprSr scalerAl. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) mathcomp(path choice fintype tuple finset bigop poly polydiv) CoqEAL(hrel param refinements poly_op)