fact: Definition PEevalR : list R -> PEZ -> R := PEeval ring0 ring1 add mul sub opp (gen_phiZ ring0 ring1 add mul opp) N.to_nat pow.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool Algebra_syntax Ncring Ncring_initial Ncring_tac Integral_domain ZArith Lia