proposition: Lemma PaddX_ok2 : forall P2, (forall P l, (P2 ++ P) @ l == P2 @ l + P @ l) /\ (forall P k n l, (PaddX Padd P2 k n P) @ l == P2 @ l * pow_pos (nth 0 k l) n + P @ l).
proof: Proof. induction P2 as [|? IH1 ??? IH2];simpl;intros. - split. + intros. apply PaddCl_ok. + intros P. induction P as [|? IH'1 ??? IH'2]. * unfold PaddX. intros. now rewrite mkPX_ok. * intros. simpl. destruct (Pos.compare_spec k p) as [Hh|Hh|Hh]. -- destr_pos_sub H1h; subst. ++ rewrite mkPX_ok, PaddCl_ok. now rewrite_db rsimpl. ++ rewrite mkPX_ok, IH'1, Pos.add_comm, pow_pos_add. now rewrite_db rsimpl. ++ rewrite mkPX_ok, PaddCl_ok, mkPX_ok, Pphi0, Pos.add_comm, pow_pos_add. now rewrite_db rsimpl. -- rewrite mkPX_ok, IH'2. rewrite_db rsimpl. now rewrite (ring_add_comm (_ * _)). -- assert (H1h := ring_morphism_eq c 0);case_eq (Ceqb c 0); intros; simpl. ++ rewrite H1h;trivial. ** rewrite ring_morphism0. now rewrite_db rsimpl. ** apply Ceqb_eq; trivial. ++ reflexivity. - decompose [and] IH1. decompose [and] IH2. clear IH1 IH2. split. + intros. rewrite H0. rewrite H1. now rewrite ring_add_assoc. + induction P. * unfold PaddX. intros. rewrite mkPX_ok. reflexivity. * intros. rewrite PaddXPX. destruct (Pos.compare_spec k p1) as [H3h|H3h|H3h]. -- destr_pos_sub H4h; subst. ++ rewrite mkPX_ok. simpl. rewrite H0, H1. now rewrite_db rsimpl. ++ rewrite mkPX_ok, IHP1. simpl. rewrite Pos.add_comm, pow_pos_add. now rewrite_db rsimpl. ++ rewrite mkPX_ok. simpl. rewrite H0, H1. rewrite mkPX_ok, Pphi0. rewrite Pos.add_comm, pow_pos_add. now rewrite_db rsimpl. -- rewrite mkPX_ok. simpl. rewrite IHP2. now rewrite ring_add_comm, <- ring_add_assoc, (ring_add_comm (_ @ _)). -- now rewrite mkPX_ok. Qed.
imports: Setoid BinList BinPos BinNat BinInt Ring_polynom Ncring