fact: Definition poly_of_seqpoly (sp : seqpoly R) : {poly R} := \poly_(i < size sp) nth 0 sp i.
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)