proposition: Theorem normalise_ps_adjust_add : ∀ ps₁ ps₂ n n₁ n₂ k₁ k₂, normalise_ps (adjusted_ps_add (adjust_ps (n + n₁) k₁ ps₁) (adjust_ps (n + n₂) k₂ ps₂)) ≐ normalise_ps (adjusted_ps_add (adjust_ps n₁ k₁ ps₁) (adjust_ps n₂ k₂ ps₂)).
proof: Proof. intros ps₁ ps₂ n n₁ n₂ k₁ k₂. replace (n + n₁)%nat with (n + n₁ * Pos.to_nat 1)%nat . replace (n + n₂)%nat with (n + n₂ * Pos.to_nat 1)%nat . replace k₁ with (1 * k₁)%positive by reflexivity. rewrite <- ps_adjust_adjust. replace k₂ with (1 * k₂)%positive by reflexivity. rewrite <- ps_adjust_adjust. do 2 rewrite Pos.mul_1_l. rewrite normalise_ps_adjust; reflexivity. rewrite Nat.mul_1_r; reflexivity. rewrite Nat.mul_1_r; reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series Ps_add