proposition: Lemma c_mult_lin : forall (p : RX) c d, _C_ c[*] (d[+X*]p) [=] c[*]d[+X*]_C_ c[*]p.
proof: Proof. intros. pattern p in |- *. apply cpoly_induc. simpl in |- *. repeat split; algebra. intros. simpl in |- *. repeat split; algebra. change ((cpoly_mult_cr R p0 c:RX) [=] (cpoly_mult_cr R p0 c:RX)[+][0]) in |- *. algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational