proposition: Lemma Zeval_formula_compat' : forall env f, Zeval_formula env Tauto.isProp f <-> Zeval_formula' env f.
proof: Proof. intros env f. unfold Zeval_formula. destruct f as [Flhs Fop Frhs]. repeat rewrite Zeval_expr_compat. unfold Zeval_formula' ; simpl. unfold eval_expr. generalize (eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) (fun x : N => x) (pow_N 1 Z.mul) env Flhs). generalize ((eval_pexpr Z.add Z.mul Z.sub Z.opp (fun x : Z => x) (fun x : N => x) (pow_N 1 Z.mul) env Frhs)). destruct Fop ; simpl; intros; intuition auto using Z.le_ge, Z.ge_le, Z.lt_gt, Z.gt_lt. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing