fact: Fixpoint zxfpx (p:zx) : fpx := match p with | cpoly_zero _ => (cpoly_zero fp : fpx) | cpoly_linear _ c p1 => (zfp c)[+X*](zxfpx p1) end.
imports: CoRN.model.Zmod.Zm CoRN.model.rings.Zring CoRN.algebra.CPoly_Degree