proposition: Theorem is_the_greatest_series_x_power_equiv : ∀ 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 ↔ match series_order s (S n) with | fin _ => is_a_series_in_x_power s n k ∧ (∀ u, (1 < u)%nat → ∃ n', ¬(u * k | nth_series_order K s n n')) | ∞ => k = O end.
proof: Proof. intros s b k. split; intros H. remember (series_order s (S b)) as p eqn:Hp₁ . symmetry in Hp₁. destruct p as [p| ]; [ idtac | assumption ]. destruct H as (Hp, Hnp). split; [ assumption | idtac ]. intros n Hn. destruct n; [ exfalso; revert Hn; apply Nat.nlt_0_r | idtac ]. destruct n; [ exfalso; revert Hn; apply Nat.lt_irrefl | clear Hn ]. destruct k. exfalso. unfold is_a_series_in_x_power in Hp. pose proof (Hnp 2%nat (Nat.lt_0_succ 1%nat)) as H. destruct H as (m, H). pose proof (Hp m) as Hm. destruct Hm as (q, Hq). rewrite Nat.mul_0_r in Hq. rewrite Hq in H. apply H. exists O; reflexivity. apply Hnp. simpl; rewrite <- Nat.add_succ_l. apply Nat.lt_add_pos_r, Nat.lt_0_succ. remember (series_order s (S b)) as p eqn:Hp₁ . symmetry in Hp₁. destruct p as [p| ]; [ idtac | assumption ]. destruct H as (Hp, Hnp). split; [ assumption | idtac ]. intros k₁ Hk₁. remember (Nat.lcm k k₁) as kk eqn:Hkk . remember Hkk as Hk; clear HeqHk. pose proof (Nat_divides_lcm_l k k₁) as Hdl. destruct Hdl as (u, Hu). rewrite <- Hkk in Hu. destruct u. simpl in Hu. rewrite Hu in Hk. symmetry in Hk. apply Nat.lcm_eq_0 in Hk. destruct Hk as [Hk| Hk]. subst k. pose proof Nat.lt_1_2 as H. apply Hnp in H. destruct H as (n, Hn). rewrite Nat.mul_0_r in Hn. unfold is_a_series_in_x_power in Hp. exfalso; apply Hn, Hp. subst k₁. exfalso; revert Hk₁; apply Nat.nlt_0_r. destruct u. rewrite Nat.mul_1_l in Hu. move Hu at top; subst kk. rewrite Hk in Hk₁. apply Nat.nle_gt in Hk₁. exfalso; apply Hk₁. rewrite Nat.lcm_comm. destruct k. unfold is_a_series_in_x_power in Hp. pose proof (Hp O) as H. simpl in H. rewrite Hp₁ in H. destruct H as (c, Hc). rewrite Nat.mul_0_r in Hc. discriminate Hc. apply Nat_le_lcm_l; auto with Arith. destruct k. unfold is_a_series_in_x_power in Hp. pose proof (Hp O) as H. simpl in H. rewrite Hp₁ in H. destruct H as (c, Hc). rewrite Nat.mul_0_r in Hc. discriminate Hc. assert (1 < S (S u))%nat as H₁. apply lt_n_S, Nat.lt_0_succ. apply Hnp in H₁. destruct H₁ as (m, Hm). rewrite <- Hu, Hkk in Hm. exists m. intros H₁; apply Hm. unfold is_a_series_in_x_power in Hp. pose proof (Hp m) as H₂. apply Nat_lcm_divides; auto with Arith. intros H; rewrite H in Hk₁. exfalso; revert Hk₁; apply Nat.nlt_0_r. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series