fact: Definition seqpoly_of_poly (p : {poly R}) : seqpoly R := polyseq p.
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)