proposition: Theorem normalise_sound : forall (env : PolEnv) (f : Formula C), eval_formula env f <-> eval_nformula env (normalise f).
proof: Proof. intros env f; destruct f as [lhs op rhs]; simpl in *. destruct op; simpl in *; rewrite eval_pol_sub ; rewrite <- eval_pol_norm ; rewrite <- eval_pol_norm. - symmetry. now apply (Rminus_eq_0 sor). - rewrite (Rminus_eq_0 sor). tauto. - now apply (Rle_le_minus sor). - now apply (Rle_le_minus sor). - now apply (Rlt_lt_minus sor). - now apply (Rlt_lt_minus sor). Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl