proposition: Theorem ps_normal_adjust_eq : ∀ ps n k, normalise_ps ps ≐ normalise_ps (adjust_ps n k ps).
proof: Proof. intros ps n k. unfold normalise_ps; simpl. rewrite series_order_shift. rewrite series_order_stretch_0. rewrite Nbar.add_comm, Nbar.mul_comm. remember (series_order (ps_terms ps) 0) as m eqn:Hm . symmetry in Hm. destruct m as [m| ]; simpl; [ idtac | reflexivity ]. rewrite greatest_series_x_power_shift. rewrite Nat2Z.inj_add, Z.add_assoc. rewrite Z.add_shuffle0. rewrite Z.sub_add. rewrite Nat2Z.inj_mul, positive_nat_Z. rewrite <- Z.mul_add_distr_r. rewrite Z.mul_comm. remember (series_order (ps_terms ps) (S m)) as p eqn:Hp . symmetry in Hp. remember (greatest_series_x_power K (ps_terms ps) m) as x. pose proof (gcd_ps_is_pos m x ps) as Hgp; subst x. destruct p as [p| ]. erewrite greatest_series_x_power_stretch. unfold gcd_ps. remember (Zpos k)%Z as kp; simpl. rewrite Nat2Z.inj_add. rewrite Z.sub_add_simpl_r_r. rewrite Nat2Z.inj_mul. rewrite Nat2Z.inj_mul. rewrite positive_nat_Z. rewrite <- Z.mul_add_distr_r. rewrite Pos2Z.inj_mul. rewrite Z.gcd_mul_mono_r_nonneg; [ idtac | apply Pos2Z.is_nonneg ]. subst kp. rewrite Z.mul_comm. rewrite Z.gcd_mul_mono_l_nonneg; [ idtac | apply Pos2Z.is_nonneg ]. rewrite Z.div_mul_cancel_l. rewrite <- Pos2Z.inj_mul, Pos.mul_comm, Pos2Z.inj_mul. rewrite Z.div_mul_cancel_l. unfold normalise_series. rewrite Z2Pos.inj_mul; [ idtac | apply Pos2Z.is_pos | idtac ]. rewrite Pos.mul_comm. rewrite series_shrink_shrink. rewrite series_left_shift_shift. rewrite Nat.add_sub. rewrite series_left_shift_stretch. rewrite series_shrink_stretch. reflexivity. rewrite Nat.add_comm; apply Nat.le_add_r. assumption. unfold gcd_ps in Hgp. intros H; rewrite H in Hgp. revert Hgp; apply Z.lt_irrefl. apply Pos2Z_ne_0. unfold gcd_ps in Hgp. intros H; rewrite H in Hgp. revert Hgp; apply Z.lt_irrefl. apply Pos2Z_ne_0. intros H; rewrite H in Hp; discriminate Hp. rewrite ncrl_inf_gsxp; [ idtac | assumption ]. rewrite greatest_series_x_power_stretch_inf; auto. rewrite gcd_ps_0_m. rewrite gcd_ps_0_m. remember Z.mul as g; simpl; subst g. rewrite Nat2Z.inj_add. rewrite Nat2Z.inj_mul. rewrite positive_nat_Z. rewrite Z.sub_add_simpl_r_r. rewrite <- Z.mul_add_distr_r. rewrite Pos2Z.inj_mul. rewrite Z.gcd_mul_mono_r_nonneg; [ idtac | apply Pos2Z.is_nonneg ]. rewrite Z.mul_comm. rewrite Z.abs_mul. remember Z.mul as g; simpl; subst g. rewrite Z.div_mul_cancel_l. rewrite <- Pos2Z.inj_mul, Pos.mul_comm, Pos2Z.inj_mul. rewrite Z.div_mul_cancel_l. unfold normalise_series. rewrite Z2Pos.inj_mul; [ idtac | apply Pos2Z.is_pos | idtac ]. rewrite Pos.mul_comm. rewrite series_shrink_shrink. rewrite series_left_shift_shift. rewrite Nat.add_sub. rewrite series_left_shift_stretch. rewrite series_shrink_stretch. reflexivity. rewrite Nat.add_comm; apply Nat.le_add_r. apply Z.abs_pos. intros H. apply Z.gcd_eq_0_r in H. revert H; apply Pos2Z_ne_0. intros H. apply -> Z.abs_0_iff in H. apply Z.gcd_eq_0_r in H. revert H; apply Pos2Z_ne_0. apply Pos2Z_ne_0. intros H. apply -> Z.abs_0_iff in H. apply Z.gcd_eq_0_r in H. revert H; apply Pos2Z_ne_0. apply Pos2Z_ne_0. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series