proposition: Lemma norm_subst_ok : forall n l lpe pe, interp_PElist l lpe -> PEeval l pe == (norm_subst n (mk_monpol_list lpe) pe)@l.
proof: Proof. intros;apply norm_subst_spec. apply interp_PElist_ok;trivial. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory