proposition: Theorem negate_correct : forall (env : PolEnv) (f : Formula C), eval_formula env f <-> ~ (eval_nformula env (negate f)).
proof: Proof. intros env f; destruct f as [lhs op rhs]; simpl. destruct op; simpl in *; rewrite eval_pol_sub ; rewrite <- eval_pol_norm ; rewrite <- eval_pol_norm. - symmetry. rewrite (Rminus_eq_0 sor). split; intro H; [symmetry; now apply -> (Req_dne sor) | symmetry in H; now apply <- (Req_dne sor)]. - rewrite (Rminus_eq_0 sor). split; intro; now apply (Rneq_symm sor). - rewrite <- (Rlt_lt_minus sor). now rewrite <- (Rle_ngt sor). - rewrite <- (Rlt_lt_minus sor). now rewrite <- (Rle_ngt sor). - rewrite <- (Rle_le_minus sor). now rewrite <- (Rlt_nge sor). - rewrite <- (Rle_le_minus sor). now rewrite <- (Rlt_nge sor). Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl