proposition: Lemma Zeval_expr_compat : forall env e, Zeval_expr env e = eval_expr env e.
proof: Proof. intros env e; induction e ; simpl ; try congruence. - reflexivity. - rewrite ZNpower. congruence. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing