proposition: Lemma eval_nformula_split : forall env p, eval_nformula env (p,NonStrict) \/ eval_nformula env (popp p,NonStrict).
proof: Proof. unfold popp. simpl. intros. rewrite (eval_pol_opp Zsor ZSORaddon). rewrite Z.opp_nonneg_nonpos. apply Z.le_ge_cases. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory Wf_nat