proposition: Lemma mkPX_ok : forall l P i n Q, (mkPX P i n Q)@l == P@l * (pow_pos (nth 0 i l) n) + Q@l.
proof: Proof. intros l P i n Q;unfold mkPX. destruct P;try (simpl;reflexivity). - assert (Hh := ring_morphism_eq c 0). simpl; case_eq (Ceqb c 0);simpl;try reflexivity. intros. rewrite Hh. + rewrite ring_morphism0. now rewrite_db rsimpl. + apply Ceqb_eq. trivial. - destruct (Pos.compare_spec i p). + subst. assert (Hh := @Peq_ok P3 P0). case_eq (P3=? P0). * intro. simpl. rewrite Hh. -- rewrite Pos.add_comm, pow_pos_add, Pphi0. now rewrite_db rsimpl. -- trivial. * intros. reflexivity. + reflexivity. + reflexivity. Qed.
imports: Setoid BinList BinPos BinNat BinInt Ring_polynom Ncring