proposition: Lemma xnormalise_correct : forall env f, (make_conj (fun x => eval_nformula env x -> False) (xnormalise 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. - apply eq_cnf. - unfold not. tauto. - rewrite le_neg. iff_ring. - rewrite le_neg. rewrite lt_le_iff. iff_ring. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing