proposition: Lemma cpoly_mult_cr_dist : forall p q c, cpoly_mult_cr_cs (cpoly_plus_cs p q) c [=] cpoly_plus_cs (cpoly_mult_cr_cs p c) (cpoly_mult_cr_cs q c).
proof: Proof. intros. pattern p, q in |- *. apply cpoly_double_comp_ind. intros. apply eq_transitive_unfolded with (cpoly_mult_cr_cs (cpoly_plus_cs p1 q1) c). apply eq_symmetric_unfolded. apply cpoly_mult_cr_wd. apply cpoly_plus_op_wd. assumption. assumption. algebra. astepl (cpoly_plus_cs (cpoly_mult_cr_cs p1 c) (cpoly_mult_cr_cs q1 c)). apply cpoly_plus_op_wd. apply cpoly_mult_cr_wd; algebra. apply cpoly_mult_cr_wd; algebra. repeat rewrite cpoly_zero_plus. algebra. intros. repeat rewrite cpoly_lin_mult_cr. repeat rewrite cpoly_lin_plus_lin. apply: _cpoly_lin_eq_lin. split; algebra. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational