proposition: Lemma PmulC_ok c P l : (PmulC P c)@l == P@l * [c].
proof: Proof. unfold PmulC. case ceqb_spec; intros H. - rewrite H; Esimpl. - case ceqb_spec; intros H'. + rewrite H'; Esimpl. + apply PmulC_aux_ok. Qed.
imports: Setoid Morphisms BinList BinPos BinNat BinInt Ring_theory