fact: Definition shift_poly n : {poly R} -> {poly R} := *%R^~ 'X^n.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div seq) mathcomp(zmodp path choice fintype tuple finset ssralg) mathcomp(bigop poly polydiv)