proposition: Lemma PmulC_ok : forall c P l, (PmulC P c)@l == P@l * [c].
proof: Proof. intros c P l; unfold PmulC. assert (Hh:= ring_morphism_eq c 0);case_eq (c =? 0). - intros. rewrite Hh. + now rewrite Pphi0, ring_morphism0, ring_mul_0_r. + now apply Ceqb_eq. - assert (H1h:= ring_morphism_eq c 1);case_eq (c =? 1);intros. + rewrite H1h. * now rewrite ring_morphism1, ring_mul_1_r. * now apply Ceqb_eq. + apply PmulC_aux_ok. Qed.
imports: Setoid BinList BinPos BinNat BinInt Ring_polynom Ncring