proposition: Lemma eval_pol_add : forall env lhs rhs, eval_pol env (padd lhs rhs) == eval_pol env lhs + eval_pol env rhs.
proof: Proof. intros. apply (Padd_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