fact: Definition RseqpolyC : {poly R} -> seq C -> Type := (Rseqpoly \o list_R rAC)%rel.
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)