proposition: Theorem ps_series_order_inf_iff : ∀ ps, series_order (ps_terms ps) 0 = ∞ ↔ (ps = 0)%ps.
proof: Proof. intros ps. split; intros H. constructor. unfold normalise_ps; simpl. rewrite H. remember (series_order 0%ser 0) as n eqn:Hn . symmetry in Hn. destruct n as [n| ]; [ idtac | reflexivity ]. apply series_order_iff in Hn. simpl in Hn. destruct Hn as (_, Hn). exfalso; apply Hn; reflexivity. inversion H; subst. apply series_order_iff; simpl; intros i. unfold normalise_ps in H0; simpl in H0. remember (series_order 0%ser 0) as n eqn:Hn . symmetry in Hn. destruct n as [n| ]. exfalso; clear H0. apply series_order_iff in Hn. simpl in Hn. destruct Hn as (_, Hn). apply Hn; reflexivity. remember (series_order (ps_terms ps) 0) as m eqn:Hm . symmetry in Hm. destruct m as [m| ]. inversion_clear H0. simpl in H1, H2, H3. remember (greatest_series_x_power K (ps_terms ps) m) as p eqn:Hp . remember (gcd_ps m p ps) as g eqn:Hg . unfold normalise_series in H3. inversion_clear H3. apply series_order_iff in Hm. simpl in Hm. destruct Hm as (Hz, Hnz). destruct (lt_dec i m) as [H₁| H₁]; [ apply Hz; assumption | idtac ]. apply Nat.nlt_ge in H₁. destruct (zerop ((i - m) mod Z.to_nat g)) as [H₂| H₂]. apply Nat.mod_divides in H₂. destruct H₂ as (c, Hc). pose proof (H0 c) as Hi. rewrite series_nth_series_0 in Hi. rewrite <- series_nth_mul_shrink in Hi. rewrite Pos2Nat_to_pos in Hi. rewrite <- Hc in Hi. rewrite <- series_nth_add_left_shift in Hi. rewrite Nat.sub_add in Hi; assumption. rewrite Hg; apply gcd_ps_is_pos. pose proof (gcd_ps_is_pos m p ps) as H₃. rewrite <- Hg in H₃. rewrite <- Z2Nat.inj_0. intros H₄. apply Z2Nat.inj in H₄; [ idtac | idtac | reflexivity ]. rewrite H₄ in H₃; revert H₃; apply Z.lt_irrefl. apply Z.lt_le_incl; assumption. symmetry in Hp. apply greatest_series_x_power_iff in Hp. remember (series_order (ps_terms ps) (S m)) as q eqn:Hq . symmetry in Hq. destruct q as [q| ]. destruct Hp as (Hxp, Hnxp). eapply series_null_power; [ eassumption | idtac ]. apply Nat.sub_gt in H₂; rewrite Nat.sub_0_r in H₂. intros H₃; apply H₂; clear H₂. pose proof (gcd_ps_is_pos m p ps) as Hgp. rewrite <- Hg in Hgp. unfold gcd_ps in Hg. remember (ps_ordnum ps + Z.of_nat m)%Z as x. remember (Z.gcd x (Zpos (ps_polydo ps))) as z. pose proof (Z.gcd_divide_r z (Z.of_nat p)) as H₄. rewrite <- Hg in H₄. apply omod_divide in H₃; auto with Arith. apply Nat.mod_divide; auto with Arith. intros H₅. rewrite <- Z2Nat.inj_0 in H₅. apply Z2Nat.inj in H₅. rewrite H₅ in Hgp; revert Hgp; apply Z.lt_irrefl. apply Z.lt_le_incl; assumption. reflexivity. eapply Nat.divide_trans; [ idtac | eassumption ]. destruct H₄ as (c, Hc). exists (Z.to_nat c). rewrite <- Z2Nat.inj_mul. rewrite <- Hc. rewrite Nat2Z.id; reflexivity. apply <- Z.mul_le_mono_pos_r; [ idtac | eassumption ]. rewrite <- Hc; simpl. apply Nat2Z.is_nonneg. apply Z.lt_le_incl; assumption. destruct p; auto with Arith. unfold is_a_series_in_x_power in Hxp. pose proof (Hxp O) as H₅; simpl in H₅. rewrite Hq in H₅. destruct H₅ as (c, Hc). rewrite Nat.mul_0_r in Hc; discriminate Hc. destruct (eq_nat_dec i m) as [H₃| H₃]. subst i. rewrite Nat.sub_diag in H₂; simpl in H₂. rewrite Nat.mod_0_l in H₂. exfalso; revert H₂; apply Nat.lt_irrefl. pose proof (gcd_ps_is_pos m p ps) as H₃. rewrite <- Hg in H₃. intros H₄. rewrite <- Z2Nat.inj_0 in H₄. apply Z2Nat.inj_iff in H₄. rewrite H₄ in H₃. exfalso; revert H₃; apply Z.lt_irrefl. apply Z.lt_le_incl; assumption. reflexivity. apply series_order_iff in Hq. simpl in Hq. pose proof (Hq (i - S m)%nat) as H₄. rewrite <- Nat.add_succ_r in H₄. rewrite <- Nat.sub_succ_l in H₄. rewrite Nat.sub_succ in H₄. rewrite Nat.add_sub_assoc in H₄; auto with Arith. rewrite Nat.add_comm, Nat.add_sub in H₄. assumption. apply Nat.neq_sym in H₃. apply Nat_le_neq_lt; assumption. apply series_order_iff in Hm. simpl in Hm. apply Hm. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series