proposition: Theorem normalised_exists_adjust : ∀ ps ps₁, series_order (ps_terms ps) 0 ≠ ∞ → normalise_ps ps = ps₁ → ∃ n k, eq_ps_strong ps (adjust_ps n k ps₁).
proof: Proof. intros ps ps₁ Hnz Heq. unfold normalise_ps in Heq. remember (series_order (ps_terms ps) 0) as len₁. symmetry in Heqlen₁. destruct len₁ as [len₁| ]; [ idtac | exfalso; apply Hnz; reflexivity ]. subst ps₁. unfold adjust_ps; simpl. remember (greatest_series_x_power K (ps_terms ps) len₁) as k₁. remember (gcd_ps len₁ k₁ ps) as g. symmetry in Heqg. destruct g as [| g| g]; simpl. unfold gcd_ps in Heqg. rewrite Z.gcd_comm, Z.gcd_assoc in Heqg. apply Z.gcd_eq_0_r in Heqg. exfalso; revert Heqg; apply Pos2Z_ne_0. exists len₁, g. constructor; simpl. unfold gcd_ps in Heqg. remember (ps_ordnum ps + Z.of_nat len₁)%Z as v. remember (Zpos (ps_polydo ps))%Z as c. pose proof (Z.gcd_divide_l (Z.gcd v c) (Z.of_nat k₁)) as H₁. destruct H₁ as (a, Ha). rewrite Heqg in Ha. pose proof (Z.gcd_divide_l v c) as H₁. destruct H₁ as (b, Hb). rewrite Ha in Hb. rewrite Z.mul_assoc in Hb. rewrite Hb. rewrite Z.div_mul; [ idtac | apply Pos2Z_ne_0 ]. rewrite <- Hb. rewrite Heqv. rewrite Z.add_simpl_r. reflexivity. unfold gcd_ps in Heqg. remember (ps_ordnum ps + Z.of_nat len₁)%Z as v. remember (Zpos (ps_polydo ps)) as c. pose proof (Z.gcd_divide_l (Z.gcd v c) (Z.of_nat k₁)) as H₁. destruct H₁ as (a, Ha). rewrite Heqg in Ha. pose proof (Z.gcd_divide_r v c) as H₁. destruct H₁ as (b, Hb). rewrite Ha in Hb. rewrite Z.mul_assoc in Hb. rewrite Hb. rewrite Z.div_mul; [ idtac | apply Pos2Z_ne_0 ]. replace g with (Z.to_pos (Zpos g)) by apply Pos2Z.id. rewrite <- Z2Pos.inj_mul. rewrite <- Hb. rewrite Heqc; simpl. reflexivity. apply Z.mul_lt_mono_pos_r with (p := Zpos g). apply Pos2Z.is_pos. rewrite <- Hb; simpl. rewrite Heqc; apply Pos2Z.is_pos. apply Pos2Z.is_pos. unfold normalise_series. rewrite series_stretch_shrink. rewrite series_shift_left_shift; [ reflexivity | apply Heqlen₁ ]. rewrite greatest_series_x_power_left_shift. rewrite Nat.add_0_r. rewrite <- Heqk₁. unfold gcd_ps in Heqg. remember (ps_ordnum ps + Z.of_nat len₁)%Z as x. remember (Zpos (ps_polydo ps))%Z as y. pose proof (Z.gcd_divide_r (Z.gcd x y) (Z.of_nat k₁)) as H. rewrite Heqg in H. destruct H as (c, Hc). exists (Z.to_nat c). rewrite <- Z2Nat_inj_mul_pos_r. rewrite <- Hc. rewrite Nat2Z.id; reflexivity. exfalso. pose proof (Zlt_neg_0 g) as H. rewrite <- Heqg in H. unfold gcd_ps in H. apply Z.nle_gt in H. apply H, Z.gcd_nonneg. Qed.
imports: Utf8 QArith NPeano NbarM Misc Field2 Power_series Puiseux_series Ps_add