proposition: Lemma eval_pol_norm : forall env e, eval_expr env e = eval_pol env (normZ e) .
proof: Proof. intros. apply (eval_pol_norm Zsor ZSORaddon). Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing