proposition: Theorem ps_ordnum_adjust_mul_add₂_distr_l : ∀ ps₁ ps₂ ps₃, ps_ordnum (adjust_ps 0 (ps_polydo ps₁) (ps₁ * ps_add₂ ps₂ ps₃)%ps) = ps_ordnum (adjust_ps 0 1 (ps_add₂ (ps₁ * ps₂)%ps (ps₁ * ps₃)%ps)).
proof: Proof. intros ps₁ ps₂ ps₃; simpl. unfold cm; simpl. unfold cm_factor. f_equal. rewrite Z.mul_1_r. 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 Pos2Z.inj_mul. do 3 rewrite Z.mul_assoc. rewrite Z.mul_sub_distr_r. do 3 rewrite <- positive_nat_Z. do 5 rewrite Z.mul_add_distr_r. rewrite Z.mul_sub_distr_r. do 2 rewrite <- Nat2Z.inj_mul. do 2 rewrite <- Z2Nat_inj_mul_pos_r. do 2 rewrite Z.mul_sub_distr_r. do 3 rewrite positive_nat_Z. rewrite Z.add_sub_assoc. f_equal. rewrite Z.mul_shuffle0. apply Z.add_cancel_l. rewrite <- Z.mul_assoc, Z.mul_shuffle0, Z.mul_assoc. reflexivity. do 2 f_equal. 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₁ * Zpos c₂)%Z as x. replace (v₁ * Zpos c₂ * Zpos c₁ * Zpos c₃)%Z with x by (subst; ring). rewrite Z.add_min_distr_l. rewrite Z.add_add_simpl_l_l. clear x Heqx. 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