fact: Definition Zeval_formula (env : PolEnv Z) (k: Tauto.kind) (f : Formula Z):= let (lhs, op, rhs) := f in (Zeval_op2 k op) (Zeval_expr env lhs) (Zeval_expr env rhs).
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing