proposition: Theorem ps_terms_adjust_mul_add₂_distr_l : ∀ ps₁ ps₂ ps₃, (ps_terms (adjust_ps 0 (ps_polydo ps₁) (ps₁ * ps_add₂ ps₂ ps₃)%ps) = ps_terms (adjust_ps 0 1 (ps_add₂ (ps₁ * ps₂)%ps (ps₁ * ps₃)%ps)))%ser.
proof: Proof. intros ps₁ ps₂ ps₃; simpl. unfold cm; simpl. unfold cm_factor. do 2 rewrite series_shift_0. rewrite series_stretch_1. remember (ps_ordnum ps₁) as v₁. remember (ps_polydo ps₂) as c₂. remember (ps_ordnum ps₂) as v₂. remember (ps_polydo ps₁) as c₁. remember (ps_ordnum ps₃) as v₃. remember (ps_polydo ps₃) as c₃. do 3 rewrite series_stretch_mul. do 6 rewrite <- series_stretch_stretch. rewrite series_stretch_add_distr. rewrite series_mul_add_distr_l. symmetry. rewrite series_mul_comm, series_shift_mul, series_mul_comm. rewrite series_add_comm. rewrite series_mul_comm, series_shift_mul, series_mul_comm. do 2 rewrite Pos2Z.inj_mul. do 2 rewrite Z.mul_assoc. do 4 rewrite Z.mul_add_distr_r. remember (v₁ * Zpos c₃ * Zpos c₁ * Zpos c₂)%Z as x. replace (v₁ * Zpos c₂ * Zpos c₁ * Zpos c₃)%Z with x by (subst x; ring). do 2 rewrite Z.add_min_distr_l. do 2 rewrite Z.add_add_simpl_l_l. clear x Heqx. do 2 rewrite stretch_shift_series_distr. do 2 rewrite <- Z2Nat_inj_mul_pos_r. rewrite Pos2Z.inj_mul. do 2 rewrite Z.mul_assoc. do 4 rewrite Z.mul_sub_distr_r. 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 ]. rewrite series_add_comm. do 2 rewrite <- series_stretch_stretch. rewrite Pos.mul_assoc. rewrite Pos_mul_shuffle0. remember (v₂ * Zpos c₁ * Zpos c₁ * Zpos c₃)%Z as x. replace (v₂ * Zpos c₃ * Zpos c₁ * Zpos c₁)%Z with x by (subst; ring). subst x. remember (v₃ * Zpos c₁ * Zpos c₁ * Zpos c₂)%Z as x. replace (v₃ * Zpos c₂ * Zpos c₁ * Zpos c₁)%Z with x by (subst; ring). subst x. remember (c₁ * c₃ * c₁)%positive as x. rewrite Pos_mul_shuffle0 in Heqx. subst x. remember (c₁ * c₂ * c₁)%positive as x. rewrite Pos_mul_shuffle0 in Heqx. subst x. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat