proposition: Theorem ps_terms_add_assoc : ∀ ps₁ ps₂ ps₃, (ps_terms_add (ps₁ + ps₂)%ps ps₃ = ps_terms_add ps₁ (ps₂ + ps₃)%ps)%ser.
proof: Proof. intros ps₁ ps₂ ps₃. constructor; intros i. unfold ps_terms_add. remember adjust_series as g; simpl. unfold cm_factor, cm. unfold ps_terms_add; simpl. unfold ps_ordnum_add; simpl. unfold cm_factor, cm. remember (ps_ordnum ps₁) as v₁ eqn:Hv₁ . remember (ps_ordnum ps₂) as v₂ eqn:Hv₂ . remember (ps_ordnum ps₃) as v₃ eqn:Hv₃ . remember (ps_polydo ps₁) as c₁. remember (ps_polydo ps₂) as c₂. remember (ps_polydo ps₃) as c₃. subst g; unfold adjust_series. do 2 rewrite series_stretch_add_distr. do 2 rewrite series_shift_add_distr. do 4 rewrite stretch_shift_series_distr. do 4 rewrite <- series_stretch_stretch; try apply Pos2Nat_ne_0. do 4 rewrite series_shift_shift. do 4 rewrite <- Z2Nat_inj_mul_pos_r. do 4 rewrite Z.mul_sub_distr_r. do 2 rewrite Pos2Z.inj_mul, Z.mul_assoc. rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ]. rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ]. rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ]. rewrite <- Z.mul_min_distr_nonneg_r; [ idtac | apply Pos2Z.is_nonneg ]. remember (v₁ * Zpos c₂ * Zpos c₃)%Z as vcc eqn:Hvcc . remember (v₂ * Zpos c₁ * Zpos c₃)%Z as cvc eqn:Hcvc . remember (v₃ * Zpos c₂ * Zpos c₁)%Z as ccv eqn:Hccv . do 2 rewrite Z.min_assoc. rewrite Z.mul_shuffle0, <- Hccv. rewrite Z.mul_shuffle0, <- Hcvc. rewrite Pos.mul_comm. replace (c₃ * c₁)%positive with (c₁ * c₃)%positive by apply Pos.mul_comm. do 6 rewrite Z2Nat_sub_min. do 2 rewrite Z2Nat_sub_min1. do 2 rewrite Z2Nat_sub_min2. do 2 rewrite <- Z.min_assoc. do 2 rewrite Z2Nat_sub_min. simpl; rewrite rng_add_assoc; reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series