proposition: Lemma eval_nformula_dec : forall env d, (eval_nformula env d) \/ ~ (eval_nformula env d).
proof: Proof. intros env d. destruct d as [p o]; simpl. generalize (eval_pol env p); intros r. destruct o ; simpl. - apply (Req_em sor r 0). - destruct (Req_em sor r 0) ; tauto. - rewrite <- (Rle_ngt sor r 0). generalize (Rle_gt_cases sor r 0). tauto. - rewrite <- (Rlt_nge sor r 0). generalize (Rle_gt_cases sor 0 r). tauto. Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl