proposition: Theorem normalise_ps_adjust : ∀ ps₁ ps₂ n, normalise_ps (adjusted_ps_add (adjust_ps n 1 ps₁) (adjust_ps n 1 ps₂)) ≐ normalise_ps (adjusted_ps_add ps₁ ps₂).
proof: Proof. intros ps₁ ps₂ n. rewrite <- ps_adjust_adjusted. unfold normalise_ps. simpl. rewrite series_order_shift. rewrite series_stretch_1. remember (series_order (series_add (ps_terms ps₁) (ps_terms ps₂)) 0)%Nbar as x. rewrite Nbar.add_comm. destruct x as [x| ]; [ simpl | reflexivity ]. constructor; simpl. rewrite Z.mul_1_r. rewrite Nat2Z.inj_add. rewrite Z.sub_add_simpl_r_r. f_equal. rewrite series_stretch_1. remember (series_add (ps_terms ps₁) (ps_terms ps₂)) as s. symmetry in Heqx. apply series_order_iff in Heqx. simpl in Heqx. destruct Heqx as (Hz, Hnz). unfold gcd_ps. simpl. rewrite Z.mul_1_r. rewrite Nat2Z.inj_add. rewrite Z.sub_add_simpl_r_r. rewrite Pos.mul_1_r. rewrite greatest_series_x_power_shift. reflexivity. rewrite Pos.mul_1_r. f_equal. f_equal. rewrite series_stretch_1. remember (series_add (ps_terms ps₁) (ps_terms ps₂)) as s. symmetry in Heqx. unfold gcd_ps. simpl. rewrite Z.mul_1_r. rewrite Pos.mul_1_r. rewrite Nat2Z.inj_add. rewrite Z.sub_add_simpl_r_r. rewrite greatest_series_x_power_shift. reflexivity. rewrite series_stretch_1. rewrite normalise_series_add_shift. remember (series_add (ps_terms ps₁) (ps_terms ps₂)) as s. unfold gcd_ps. simpl. rewrite Z.mul_1_r. rewrite Pos.mul_1_r. rewrite Nat2Z.inj_add. rewrite Z.sub_add_simpl_r_r. rewrite greatest_series_x_power_shift. reflexivity. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series Ps_add