proposition: Lemma norm_aux_spec l pe : PEeval l pe == (norm_aux pe)@l.
proof: Proof. intros. induction pe as [| |pe1 IHpe1 pe2 IHpe2|? IHpe1 ? IHpe2|? IHpe1 ? IHpe2|? IHpe|? IHpe n0]. - reflexivity. - apply mkX_ok. - simpl PEeval. rewrite IHpe1, IHpe2. assert (H1 := norm_aux_PEopp pe1). assert (H2 := norm_aux_PEopp pe2). rewrite norm_aux_PEadd. do 2 destruct get_PEopp; rewrite ?H1, ?H2; Esimpl; add_permut. - simpl. rewrite IHpe1, IHpe2. Esimpl. - simpl. rewrite IHpe1, IHpe2. now rewrite Pmul_ok. - simpl. rewrite IHpe. Esimpl. - simpl. rewrite Ppow_N_ok by reflexivity. rewrite (rpow_pow_N pow_th). destruct n0 as [|p]; simpl; Esimpl. induction p as [p IHp|p IHp|];simpl; now rewrite ?IHp, ?IHpe, ?Pms_ok, ?Pmul_ok. Qed.
imports: Setoid Morphisms Env BinPos BinNat BinInt Ring_theory