proposition: Lemma cpoly_mult_lin : forall c p q, cpoly_mult_cs p (cpoly_linear_cs c q) [=] cpoly_plus_cs (cpoly_mult_cr_cs p c) (cpoly_linear_cs [0] (cpoly_mult_cs p q)).
proof: Proof. intros. pattern p in |- *; apply cpoly_ind_cs. repeat rewrite cpoly_zero_mult. rewrite cpoly_zero_mult_cr. rewrite cpoly_zero_plus. apply _cpoly_zero_eq_lin. algebra. intros. repeat rewrite cpoly_lin_mult. repeat rewrite cpoly_lin_mult_cr. repeat rewrite cpoly_lin_plus_lin. apply _cpoly_lin_eq_lin. split. algebra. apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_plus_cs (cpoly_mult_cr_cs p0 c) (cpoly_mult_cr_cs q c0)) (cpoly_linear_cs [0] (cpoly_mult_cs p0 q))). 2: apply eq_symmetric_unfolded. 2: apply cpoly_plus_associative. apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_plus_cs (cpoly_mult_cr_cs q c0) (cpoly_mult_cr_cs p0 c)) (cpoly_linear_cs [0] (cpoly_mult_cs p0 q))). 2: apply cpoly_plus_op_wd. 3: algebra. 2: apply cpoly_plus_commutative. apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_mult_cr_cs q c0) (cpoly_plus_cs (cpoly_mult_cr_cs p0 c) (cpoly_linear_cs [0] (cpoly_mult_cs p0 q)))). 2: apply cpoly_plus_associative. apply cpoly_plus_op_wd. algebra. assumption. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational