proposition: Lemma cpoly_cr_dist : distributive cpoly_mult_op cpoly_plus_op.
proof: Proof. unfold distributive in |- *. intros p q r. change (cpoly_mult_cs p (cpoly_plus_cs q r) [=] cpoly_plus_cs (cpoly_mult_cs p q) (cpoly_mult_cs p r)) in |- *. pattern p in |- *. apply cpoly_ind_cs. repeat rewrite cpoly_zero_mult. rewrite cpoly_zero_plus. algebra. intros. repeat rewrite cpoly_lin_mult. apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_plus_cs (cpoly_mult_cr_cs q c) (cpoly_mult_cr_cs r c)) (cpoly_plus_cs (cpoly_linear_cs [0] (cpoly_mult_cs p0 q)) (cpoly_linear_cs [0] (cpoly_mult_cs p0 r)))). apply cpoly_plus_op_wd. apply cpoly_mult_cr_dist. rewrite cpoly_lin_plus_lin. apply _cpoly_lin_eq_lin. split. algebra. assumption. clear H. apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_mult_cr_cs q c) (cpoly_plus_cs (cpoly_mult_cr_cs r c) (cpoly_plus_cs (cpoly_linear_cs [0] (cpoly_mult_cs p0 q)) (cpoly_linear_cs [0] (cpoly_mult_cs p0 r))))). apply eq_symmetric_unfolded. apply cpoly_plus_associative. apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_mult_cr_cs q c) (cpoly_plus_cs (cpoly_linear_cs [0] (cpoly_mult_cs p0 q)) (cpoly_plus_cs (cpoly_mult_cr_cs r c) (cpoly_linear_cs [0] (cpoly_mult_cs p0 r))))). apply cpoly_plus_op_wd. algebra. apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_plus_cs (cpoly_mult_cr_cs r c) (cpoly_linear_cs [0] (cpoly_mult_cs p0 q))) (cpoly_linear_cs [0] (cpoly_mult_cs p0 r))). apply cpoly_plus_associative. apply eq_transitive_unfolded with (cpoly_plus_cs (cpoly_plus_cs (cpoly_linear_cs [0] (cpoly_mult_cs p0 q)) (cpoly_mult_cr_cs r c)) (cpoly_linear_cs [0] (cpoly_mult_cs p0 r))). apply cpoly_plus_op_wd. apply cpoly_plus_commutative. algebra. apply eq_symmetric_unfolded. apply cpoly_plus_associative. apply cpoly_plus_associative. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational