proposition: Lemma ring_correct : forall n l lpe pe1 pe2, interp_PElist l lpe -> (let lmp := mk_monpol_list lpe in norm_subst n lmp pe1 ?== norm_subst n lmp pe2) = true -> PEeval l pe1 == PEeval l pe2.
proof: Proof. simpl;intros n l lpe pe1 pe2 **. do 2 (rewrite (norm_subst_ok n l lpe);trivial). apply Peq_ok;trivial. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory