proposition: Lemma norm_correct : forall (l : list R) (pe : PEZ), PEevalR l pe == PhiR l (norm pe).
proof: Proof. intros;apply (norm_aux_spec Rset Rext (Rth_ARth Rset Rext Rtheory) (gen_phiZ_morph Rset Rext Rtheory) R_power_theory). Qed.
imports: List Setoid BinPos BinList Znumtheory Morphisms Setoid Bool Algebra_syntax Ncring Ncring_initial Ncring_tac Integral_domain ZArith Lia