proposition: Theorem greatest_series_x_power_iff : ∀ α (R : ring α) (K : field R) s n k, greatest_series_x_power K s n = k ↔ match series_order s (S n) with | fin _ => is_a_series_in_x_power s n k ∧ (∀ k', (k < k')%nat → ∃ n', ¬(k' | nth_series_order K s n n')) | ∞ => k = O end.
proof: Proof. intros. unfold greatest_series_x_power. remember (nth_series_order K s n) as u eqn:Hu ; symmetry in Hu. remember (sequence_gcd_upto u) as v eqn:Hv ; symmetry in Hv. remember (sequence_diff v) as w eqn:Hw ; symmetry in Hw. remember (sequence_all_zero_from w) as t eqn:Ht ; symmetry in Ht. assert (Pv : ∀ i, v (S i) ≤ v i). intros i. induction i. subst v; simpl. remember (u O) as u0 eqn:Hu0 ; symmetry in Hu0. remember (u 1%nat) as u1 eqn:Hu1 ; symmetry in Hu1. rewrite <- Hu in Hu0, Hu1; simpl in Hu0, Hu1. remember (series_order s (S n)) as x eqn:Hx ; symmetry in Hx. destruct x as [p| ]. destruct u0; [ discriminate Hu0 | ]. apply Nat_gcd_le_r; intros H1; discriminate H1. subst u0 u1. apply Nat.le_refl. subst v; simpl; simpl in IHi. remember (u (S i)) as usi eqn:Husi ; symmetry in Husi. remember (u (S (S i))) as ussi eqn:Hussi ; symmetry in Hussi. rewrite <- Hu in Husi, Hussi; simpl in Husi, Hussi. destruct usi. destruct ussi; [ apply Nat.le_refl | ]. remember (sequence_gcd_upto u i) as x eqn:Hx . destruct x. simpl in IHi; simpl. remember (series_order s (S n)) as y eqn:Hy ; symmetry in Hy. destruct y as [p| ]; [ | discriminate Hussi ]. remember (series_order s (S (S (n + p)))) as z eqn:Hz ; symmetry in Hz. destruct z; [ | discriminate Hussi ]. apply nth_series_order_0_add with (j := S x) in Husi. rewrite Nat.add_succ_r in Husi; simpl in Husi. rewrite Husi in Hussi. discriminate Hussi. apply Nat_gcd_le_r. intros H1; discriminate H1. apply Nat_gcd_le_r. intros H1; apply Nat.gcd_eq_0_l in H1. discriminate H1. split; intros H. symmetry in H. assert (Pv2 : ∃ m g, (∀ i, m ≤ i → v i = g) ∧ (∀ i, i < m → g < v i)%nat). apply non_increasing_natural_sequence_first_limit, Pv. destruct Pv2 as (m, (g, (Pv2, Pv3))). destruct (LPO t) as [H1| (i, Hi)]. remember (series_order s (S n)) as x eqn:Hx ; symmetry in Hx. destruct x as [x| ]; [ | apply H ]. apply series_order_iff in Hx. destruct Hx as (H2, H3). pose proof (H1 m) as H4. rewrite <- Ht in H4. unfold sequence_all_zero_from in H4. destruct (LPO (λ i : nat, w (m + i)%nat)) as [H5| (i, Hi)]. discriminate H4. rewrite <- Hw in Hi. unfold sequence_diff in Hi. rewrite Pv2 in Hi; [ | apply Nat.le_add_r ]. rewrite Pv2 in Hi; [ | rewrite <- Nat.add_succ_r; apply Nat.le_add_r ]. rewrite Nat.sub_diag in Hi. exfalso; apply Hi, eq_refl. assert (H1 : v i = g). destruct (lt_eq_lt_dec i m) as [[H1| H1]| H1]. subst t; unfold sequence_all_zero_from in Hi. destruct (LPO (λ j, w (i + j)%nat)) as [H2| (j, Hj)]. subst w; unfold sequence_diff in H2. exfalso. destruct m; [ revert H1; apply Nat.nlt_0_r | ]. pose proof (H2 (m - i)%nat) as H4. rewrite Nat.add_sub_assoc in H4; [ | apply Nat.succ_le_mono, H1 ]. rewrite Nat.add_comm, Nat.add_sub in H4. apply Nat.sub_0_le, Nat.nlt_ge in H4. pose proof (Pv2 (S m) (Nat.le_refl (S m))) as H5. pose proof (Pv3 m (Nat.lt_succ_diag_r m)) as H6. rewrite H5 in H4; apply H4, H6. exfalso; apply Hi, Nat.eq_refl. apply Pv2, Nat.eq_le_incl, Nat.eq_sym, H1. apply Pv2, Nat.lt_le_incl, H1. rewrite H1 in H; subst k. remember (series_order s (S n)) as x eqn:Hx ; symmetry in Hx. destruct x as [x| ]. split. unfold is_a_series_in_x_power. rewrite Hu; intros p. apply sequence_gcd_divide with (m := m). rewrite Hv; apply Pv2. intros k Hgk. assert (H : ¬ (∀ i, (k | u i))). intros H. assert (H4 : (k | Nat.gcd (u (S i)) (v i))). apply Nat.gcd_greatest; [ apply H | ]. rewrite <- Hv; clear Hi H1. induction i; [ apply H | simpl ]. apply Nat.gcd_greatest; [ apply H | apply IHi ]. pose proof (Pv2 (S i)) as H2. rewrite <- Hv in H4, H2. simpl in H2. destruct (le_dec m (S i)) as [H3| H3]. apply H2 in H3. rewrite H3 in H4. destruct H4 as (z, Hz). rewrite Hz in Hgk. destruct z. simpl in Hz. move Hz at top; subst g. apply Nat.gcd_eq_0 in H3. destruct H3 as (H3, H4). destruct m. assert (H5 : ∀ i, u i = O). intros j. pose proof (Pv2 j (Nat.le_0_l j)) as H5. rewrite <- Hv in H5. induction j; [ apply H5 | ]. simpl in H5. apply Nat.gcd_eq_0_l in H5. apply H5. pose proof (H5 O) as H6. rewrite <- Hu in H6. simpl in H6. rewrite Hx in H6. discriminate H6. pose proof (Pv3 O (Nat.lt_0_succ m)) as H5. rewrite <- Hv in H5; simpl in H5. clear Hi H1 H2 H3. induction i. simpl in H4. rewrite H4 in H5. revert H5; apply Nat.lt_irrefl. simpl in H4. apply Nat.gcd_eq_0_r in H4. apply IHi, H4. simpl in Hgk. apply Nat.lt_add_lt_sub_l in Hgk. rewrite Nat.sub_diag in Hgk. revert Hgk; apply Nat.nlt_0_r. apply Nat.nle_gt in H3. pose proof (Pv3 (S i) H3) as H5. rewrite <- H1 in H5. apply Nat.nle_gt in H5. apply H5, Pv. destruct (LPO (λ n', u n' mod k)) as [H2| H2]. exfalso; apply H; intros j. exists (u j / k)%nat. rewrite Nat.mul_comm. apply Nat.div_exact; [ | apply H2 ]. intros H3; subst k; revert Hgk; apply Nat.nlt_0_r. destruct H2 as (j, Hj). exists j; intros (z, Hz). rewrite Hz in Hj. apply Hj, Nat.mod_mul. intros H3; subst k; revert Hgk; apply Nat.nlt_0_r. assert (H2 : ∀ i, u i = O). intros j; rewrite <- Hu. destruct j; simpl; rewrite Hx; apply eq_refl. rewrite <- Hv in H1; clear Hi. induction i; [ rewrite <- H1; apply H2 | simpl in H1 ]. rewrite H2 in H1; simpl in H1. apply IHi, H1. symmetry. remember (series_order s (S n)) as x eqn:Hx ; symmetry in Hx. destruct (LPO t) as [H3| (i, H3)]. destruct x as [x| ]; [ | apply H ]. pose proof (non_increasing_natural_sequence_first_limit v Pv) as H1. destruct H1 as (m, (l, (H1, H2))). pose proof (H3 m) as H4. rewrite <- Ht in H4; simpl in H4. unfold sequence_all_zero_from in H4. destruct (LPO (λ i, w (m + i)%nat)) as [| (i, Hi)]; [ discriminate H4 | ]. clear H4; rewrite <- Hw in Hi. exfalso; apply Hi; clear Hi. unfold sequence_diff. rewrite H1; [ | apply Nat.le_add_r ]. rewrite <- Nat.add_succ_r. rewrite H1; [ | apply Nat.le_add_r ]. apply Nat.sub_diag. destruct x as [x| ]. destruct H as (H1, H2). rewrite <- Ht in H3. unfold sequence_all_zero_from in H3. destruct (LPO (λ j, w (i + j)%nat)) as [H4| (j, Hj)]. clear H3. unfold is_a_series_in_x_power in H1. rewrite Hu in H1. rewrite <- Hw in H4. assert (H3 : ∀ j, v (i + j)%nat = v (S (i + j))). intros. pose proof (Pv (i + j)%nat) as H5. pose proof (H4 j) as H6. unfold sequence_diff in H6. apply Nat.sub_0_le in H6. apply Nat.le_antisymm; [ apply H6 | apply H5 ]. assert (H5 : (k | v i)). clear H3 H4. induction i; [ rewrite <- Hv; apply H1 | simpl ]. rewrite <- Hv; simpl; rewrite Hv. destruct IHi as (y, H3). pose proof (H1 (S i)) as H4. destruct H4 as (z, H4). rewrite H3, H4, Nat.gcd_mul_mono_r. apply Nat.divide_factor_r. assert (H7 : v i ≤ k). destruct (le_dec (v i) k) as [H7| H7]; [ apply H7 | ]. apply Nat.nle_gt in H7. apply H2 in H7. destruct H7 as (n', H7). exfalso; apply H7; clear H7. apply sequence_gcd_divide with (m := i). intros j Hij; rewrite Hv. remember (j - i)%nat as h eqn:Hh . assert (j = (i + h)%nat); [ | subst j; clear Hij Hh ]. subst h; rewrite Nat.add_sub_assoc; [ | apply Hij ]. apply eq_sym; rewrite Nat.add_comm. apply Nat.add_sub. induction h; [ rewrite Nat.add_0_r; apply Nat.eq_refl | ]. rewrite <- IHh, Nat.add_succ_r. apply eq_sym, H3. destruct H5 as (z, H5). rewrite H5; rewrite H5 in H7. destruct z. simpl in H5, H7; simpl. destruct k; [ apply eq_refl | exfalso; clear H7 ]. assert (H6 : ∀ j, v j = O). intros j. destruct (le_dec i j) as [H6| H6]. remember (j - i)%nat as h eqn:Hh . assert (j = (i + h)%nat); [ | subst j ]. subst h; rewrite Nat.add_sub_assoc; [ | apply H6 ]. apply eq_sym; rewrite Nat.add_comm. apply Nat.add_sub. induction h; [ rewrite Nat.add_0_r; apply H5 | ]. rewrite <- IHh, Nat.add_succ_r. apply eq_sym, H3. rewrite Nat.add_comm. apply eq_sym, Nat.add_sub. apply Nat.le_add_r. apply Nat.nle_gt, Nat.lt_le_incl in H6. clear H3 H4. remember (i - j)%nat as h eqn:Hh . assert (i = (h + j)%nat) by fast_omega H6 Hh. subst i. clear H6 Hh. revert j H5. induction h; intros; [ apply H5 | ]. rewrite Nat.add_succ_l, <- Nat.add_succ_r in H5. apply IHh in H5. rewrite <- Hv in H5; simpl in H5; rewrite Hv in H5. apply Nat.gcd_eq_0_r in H5; apply H5. assert (H7 : ∀ j, u j = 0%nat). intros j. induction j. pose proof (H6 O) as H7. rewrite <- Hv in H7; apply H7. pose proof (H6 (S j)) as H7. rewrite <- Hv in H7; simpl in H7; rewrite Hv in H7. apply Nat.gcd_eq_0_l in H7; apply H7. pose proof (H2 (S (S k)) (Nat.lt_succ_diag_r (S k))) as H8. destruct H8 as (n', H8). apply H8. rewrite H7. exists O. apply eq_refl. simpl in H7. destruct z; [ rewrite Nat.mul_1_l; apply eq_refl | ]. destruct k; [ rewrite Nat.mul_0_r; apply eq_refl | ]. apply Nat.le_add_le_sub_l in H7. rewrite Nat.sub_diag in H7. exfalso; revert H7; apply Nat.nle_succ_0. exfalso; apply H3, eq_refl. subst k. rewrite <- Hv; apply eq_sym. clear H3. induction i; simpl. rewrite <- Hu; simpl. rewrite Hx; apply eq_refl. rewrite IHi, Nat.gcd_comm; simpl. rewrite <- Hu; simpl. rewrite Hx; apply eq_refl. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series