proposition: Lemma norm_aux_spec : forall l pe, PEeval l pe == (norm_aux pe)@l.
proof: Proof. intros. induction pe as [ | | | |pe1 IH1 pe2 IH2|pe1 IH1 pe2 IH2|pe1 IH1 pe2 IH2|pe IH|pe IH n]; simpl. - now rewrite <- ring_morphism0. - now rewrite <- ring_morphism1. - reflexivity. - rewrite ring_morphism0, ring_morphism1. now rewrite_db rsimpl. - rewrite IH1, IH2. unfold Psub. destruct pe2; now rewrite Padd_ok. - rewrite IH1, IH2. unfold Psub. now rewrite Padd_ok, Popp_ok, ring_sub_def. - now rewrite IH1, IH2, Pmul_ok. - now rewrite IH, Popp_ok. - rewrite Ppow_N_ok; [|intros; reflexivity]. rewrite rpow_pow_N; [|now apply pow_th]. destruct n; simpl; [now rewrite ring_morphism1|]. induction p as [p IHp|p IHp|]; simpl; [| |now apply IH]. + now rewrite IHp, IH, !Pmul_ok. + now rewrite Pmul_ok, IHp. Qed.
imports: Setoid BinList BinPos BinNat BinInt Ring_polynom Ncring