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; repeat rewrite eval_pol_opp; generalize (eval_pol env e) as x; intro x. - apply eq0_cnf. - unfold not. tauto. - symmetry. rewrite (Rlt_nge sor). rewrite (Rle_le_minus sor). setoid_replace (0 - x) with (-x) by ring. tauto. - rewrite (Rle_ngt sor). symmetry. rewrite (Rlt_lt_minus sor). setoid_replace (0 - x) with (-x) by ring. tauto. Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl