proposition: Theorem normalise_ps_eq : ∀ ps, (normalise_ps ps = ps)%ps.
proof: Proof. intros ps. unfold normalise_ps. unfold normalise_ps. remember (series_order (ps_terms ps) 0) as n eqn:Hn . symmetry in Hn. destruct n as [n| ]; constructor. remember (greatest_series_x_power K (ps_terms ps) n) as x. remember (gcd_ps n x ps) as g eqn:Hg . pose proof (gcd_ps_is_pos n x ps) as Hgp; subst x. rewrite <- Hg in Hgp. unfold gcd_ps in Hg; simpl in Hg. remember (ps_ordnum ps + Z.of_nat n)%Z as x eqn:Hx . rewrite <- Z.gcd_assoc in Hg. remember (greatest_series_x_power K (ps_terms ps) n) as z. remember (Z.gcd (Zpos (ps_polydo ps)) (Z.of_nat z)) as y eqn:Hy ; subst z. rewrite ps_normal_adjust_eq with (k := Z.to_pos g) (n := n). unfold adjust_ps; simpl. unfold normalise_series. rewrite series_stretch_shrink. rewrite series_shift_left_shift; [ idtac | apply Hn ]. rewrite <- positive_nat_Z. rewrite Pos2Nat_to_pos; [ idtac | assumption ]. rewrite Z2Nat.id; [ idtac | apply Z.lt_le_incl; assumption ]. rewrite Z.mul_comm. assert (x mod g = 0)%Z as Hxk. apply Z.mod_divide. intros H; revert Hgp; rewrite H; apply Z.lt_irrefl. rewrite Hg; apply Z.gcd_divide_l. apply Z.div_exact in Hxk. rewrite <- Hxk, Hx, Z.add_simpl_r. rewrite Hy, Z.gcd_comm, <- Z.gcd_assoc in Hg. remember (greatest_series_x_power K (ps_terms ps) n) as z. pose proof (Z.gcd_divide_l (Zpos (ps_polydo ps)) (Z.gcd (Z.of_nat z) x)) as Hgc. rewrite <- Hg in Hgc. destruct Hgc as (c, Hc). rewrite Hc. rewrite Z.div_mul. rewrite <- Z2Pos.inj_mul; [ idtac | idtac | assumption ]. rewrite <- Hc; simpl. destruct ps; reflexivity. destruct c as [| c| c]. exfalso; revert Hc; apply Pos2Z_ne_0. apply Pos2Z.is_pos. simpl in Hc. destruct g as [| g| g]. exfalso; revert Hc; apply Pos2Z_ne_0. rewrite <- Pos2Z.opp_pos in Hc. apply Z.add_move_0_r in Hc. rewrite <- Pos2Z.inj_add in Hc. exfalso; revert Hc; apply Pos2Z_ne_0. apply Z.nle_gt in Hgp. exfalso; apply Hgp; apply Pos2Z.neg_is_nonpos. intros H; revert Hgp; rewrite H; apply Z.lt_irrefl. intros H1; revert Hgp; rewrite H1; apply Z.lt_irrefl. rewrite greatest_series_x_power_left_shift, Nat.add_0_r. rewrite Pos2Nat_to_pos; [ idtac | assumption ]. remember (greatest_series_x_power K (ps_terms ps) n) as t. rewrite Hy in Hg. rewrite Z.gcd_assoc in Hg. remember (Z.gcd x (Zpos (ps_polydo ps))) as u. pose proof (Z.gcd_divide_r u (Z.of_nat t)) as H. rewrite <- Hg in H. destruct H as (c, Hc). exists (Z.to_nat c). rewrite <- Z2Nat.inj_mul. rewrite <- Hc. rewrite Nat2Z.id; symmetry; apply Heqt. apply Z.mul_le_mono_pos_r with (p := g); [ assumption | idtac ]. rewrite <- Hc; simpl. apply Nat2Z.is_nonneg. apply Z.lt_le_incl; assumption. unfold normalise_ps; simpl. rewrite series_order_series_0, Hn. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Fsummation Power_series Puiseux_series Ps_add Ps_add_compat