proposition: Theorem ps_adjust_adjust : ∀ ps n₁ n₂ k₁ k₂, eq_ps_strong (adjust_ps n₁ k₁ (adjust_ps n₂ k₂ ps)) (adjust_ps (n₁ + n₂ * Pos.to_nat k₁) (k₁ * k₂) ps).
proof: Proof. intros ps n₁ n₂ k₁ k₂. unfold adjust_ps; simpl. constructor; simpl. rewrite Z.mul_sub_distr_r. rewrite Pos2Z.inj_mul, Z.mul_assoc, Z.mul_shuffle0. rewrite <- Z.sub_add_distr; f_equal. rewrite Nat2Z.inj_add, Z.add_comm; f_equal. rewrite Nat2Z.inj_mul, positive_nat_Z. reflexivity. rewrite Pos.mul_assoc, Pos_mul_shuffle0. reflexivity. rewrite stretch_shift_series_distr. rewrite series_shift_shift. rewrite series_stretch_stretch. reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series Ps_add