proposition: Lemma eval_nformula_bound_var : forall env x, env x >= 0 -> eval_nformula env (xnnormalise (bound_var x)).
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