proposition: Lemma cpoly_plus_associative : associative cpoly_plus_op.
proof: Proof. unfold associative in |- *. intros p q r. change (cpoly_plus_cs p (cpoly_plus_cs q r) [=] cpoly_plus_cs (cpoly_plus_cs p q) r) in |- *. pattern p, q, r in |- *; apply cpoly_triple_comp_ind. intros. apply eq_transitive_unfolded with (cpoly_plus_cs p1 (cpoly_plus_cs q1 r1)). apply eq_symmetric_unfolded. apply cpoly_plus_op_wd. assumption. apply cpoly_plus_op_wd. assumption. assumption. astepl (cpoly_plus_cs (cpoly_plus_cs p1 q1) r1). apply cpoly_plus_op_wd. apply cpoly_plus_op_wd. assumption. assumption. assumption. simpl in |- *. auto. intros. repeat rewrite cpoly_lin_plus_lin. apply _cpoly_lin_eq_lin. split. algebra. assumption. Qed.
imports: CoRN.algebra.CRing_Homomorphisms CoRN.tactics.Rational