proposition: Lemma eval_pol_mul : forall env lhs rhs, eval_pol env (pmul lhs rhs) == eval_pol env lhs * eval_pol env rhs.
proof: Proof. intros. apply (Pmul_ok sor.(SORsetoid) Rops_wd (Rth_ARth (SORsetoid sor) Rops_wd sor.(SORrt)) addon.(SORrm)). Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl