proposition: Lemma ring_correct : forall l pe1 pe2, (norm_subst pe1 =? norm_subst pe2) = true -> PEeval l pe1 == PEeval l pe2.
proof: Proof. simpl;intros. do 2 (rewrite (norm_subst_ok l);trivial). apply Peq_ok;trivial. Qed.
imports: Setoid BinList BinPos BinNat BinInt Ring_polynom Ncring