proposition: Lemma eval_nformula_mk_eq_pos : forall env x z t, env x = env z - env t -> eval_nformula env (xnnormalise (mk_eq_pos x z t)).
proof: Proof. intros. rewrite xnnormalise_correct. simpl. auto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory Wf_nat