proposition: Lemma xnegate_correct : forall env f, (make_conj (fun x => eval_nformula env x -> False) (xnegate f)) <-> ~ eval_nformula env f.
proof: Proof. intros env f. destruct f as [e o]; destruct o eqn:Op; cbn - [psub]; repeat rewrite eval_pol_sub; fold eval_pol; repeat rewrite eval_pol_Pc; generalize (eval_pol env e) as x; intro x. - tauto. - rewrite eq_cnf. destruct (Z.eq_decidable x 0);tauto. - rewrite lt_le_iff. tauto. - tauto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums