proposition: Lemma coef_poly_of_seqpoly (sp : seqpoly R) (i : nat) : (\poly_(j < size sp) sp`_j)`_i = sp`_i.
proof: Proof. rewrite coef_poly. have [iltp|pleqi] := ltnP i (size sp)=> //. by rewrite nth_default. 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)