proposition: Lemma eval_pol_sub : forall env lhs rhs, eval_pol env (psub lhs rhs) == eval_pol env lhs - eval_pol env rhs.
proof: Proof. intros. apply (Psub_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