proposition: Lemma PmulC_aux_ok : forall c P l, (PmulC_aux P c)@l == P@l * [c].
proof: Proof. induction P as [|? IH1 ??? IH2]; simpl; intros. - now rewrite ring_morphism_mul. - rewrite mkPX_ok, IH1, IH2, !phiCR_comm. now rewrite_db rsimpl. Qed.
imports: Setoid BinList BinPos BinNat BinInt Ring_polynom Ncring