proposition: Lemma xdenorm_correct : forall p i env, eval_pol (jump i env) p == eval_pexpr env (xdenorm (Pos.succ i) p).
proof: Proof. unfold eval_pol. intros p; induction p as [|? p IHp|p2 IHp1 ? p3 IHp2]. - simpl. reflexivity. - simpl. intros. rewrite Pos.add_succ_r. rewrite <- IHp. symmetry. rewrite Pos.add_comm. rewrite Pjump_add. reflexivity. - simpl. intros. rewrite <- IHp1, <- IHp2. unfold Env.tail , Env.hd. rewrite <- Pjump_add. rewrite Pos.add_1_r. unfold Env.nth. unfold jump at 2. rewrite <- Pos.add_1_l. rewrite (rpow_pow_N (SORpower addon)). unfold pow_N. ring. Qed.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl