proposition: Theorem ps_adjust_adjusted : ∀ ps₁ ps₂ n k, eq_ps_strong (adjust_ps n k (adjusted_ps_add ps₁ ps₂)) (adjusted_ps_add (adjust_ps n k ps₁) (adjust_ps n k ps₂)).
proof: Proof. intros ps₁ ps₂ n k. constructor; simpl; try reflexivity. rewrite series_stretch_add_distr. rewrite series_shift_add_distr. reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series Ps_add