fact: Definition splitp : nat -> {poly R} -> {poly R} * {poly R} := fun n p => (rdivp p 'X^n, rmodp p 'X^n).
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq ssralg) mathcomp(path choice fintype tuple finset bigop poly polydiv)