proposition: Lemma Ppow_pos_ok : forall l, (forall P, subst_l P@l == P@l) -> forall res P p, (Ppow_pos res P p)@l == (pow_pos_gen Pmul P p)@l * res@l.
proof: Proof. intros l subst_l_ok res P p. generalize res;clear res. induction p;simpl;intros. - rewrite subst_l_ok, !Pmul_ok, !IHp. now rewrite_db rsimpl. - rewrite Pmul_ok, !IHp. now rewrite_db rsimpl. - now rewrite subst_l_ok, Pmul_ok. Qed.
imports: Setoid BinList BinPos BinNat BinInt Ring_polynom Ncring