proposition: Lemma eval_pol_opp : forall env e, eval_pol env (popp e) == - eval_pol env e.
proof: Proof. intros. apply (Popp_ok (SORsetoid sor) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd (SORrt sor)) (SORrm addon)). Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl