proposition: Theorem null_range_length_mul_add₂_distr_l : ∀ ps₁ ps₂ ps₃, series_order (ps_terms (adjust_ps 0 (ps_polydo ps₁) (ps₁ * ps_add₂ ps₂ ps₃)%ps)) 0 = series_order (ps_terms (adjust_ps 0 1 (ps_add₂ (ps₁ * ps₂)%ps (ps₁ * ps₃)%ps))) 0.
proof: Proof. intros ps₁ ps₂ ps₃; simpl. unfold cm, cm_factor; simpl. 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. do 2 rewrite stretch_shift_series_distr. do 2 rewrite <- series_stretch_stretch. symmetry. rewrite series_mul_comm. rewrite series_shift_mul. rewrite series_add_comm. rewrite series_mul_comm. rewrite series_shift_mul. rewrite series_add_comm. replace (c₁ * c₃ * c₂)%positive with (c₁ * c₂ * c₃)%positive by apply Pos_mul_shuffle0. rewrite <- series_mul_add_distr_r. rewrite series_mul_comm. do 2 rewrite Pos2Z.inj_mul, Z.mul_assoc. do 4 rewrite Z.mul_add_distr_r. remember (v₁ * Zpos c₂ * Zpos c₁ * Zpos c₃)%Z as x eqn:Hx . 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 Hx. 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 Pos.mul_assoc. do 2 f_equal. f_equal. rewrite Pos_mul_shuffle0. do 2 f_equal. f_equal; [ ring | idtac ]. f_equal; ring. rewrite Pos_mul_shuffle0. do 2 f_equal. f_equal; [ ring | idtac ]. f_equal; ring. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat