proposition: Theorem PEsimp_ok e : (PEsimp e === e)%poly.
proof: Proof. induction e; simpl. - reflexivity. - reflexivity. - intro l; trivial. - intro l; trivial. - rewrite NPEadd_ok. now f_equiv. - rewrite NPEsub_ok. now f_equiv. - rewrite NPEmul_ok. now f_equiv. - rewrite NPEopp_ok. now f_equiv. - rewrite NPEpow_ok. now f_equiv. Qed.
imports: ZArith_base