proposition: Lemma Pmul_ok : forall P P' l, (P**P')@l == P@l * P'@l.
proof: Proof. induction P'; simpl; intros. - rewrite PmulC_ok. reflexivity. - rewrite PaddX_ok. rewrite IHP'1. rewrite IHP'2. now rewrite_db rsimpl. Qed.
imports: Setoid BinList BinPos BinNat BinInt Ring_polynom Ncring