proposition: Lemma denorm_correct : forall p env, eval_pol env p == eval_pexpr env (denorm p).
proof: Proof. unfold denorm. intros p; induction p as [| |? IHp1 ? ? IHp2]. - reflexivity. - simpl. rewrite Pos.add_1_r. apply xdenorm_correct. - simpl. intros. rewrite IHp1. unfold Env.tail. rewrite xdenorm_correct. change (Pos.succ xH) with 2%positive. rewrite (rpow_pow_N (SORpower addon)). simpl. reflexivity. Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl