proposition: Theorem greatest_series_x_power_stretch : ∀ s b k, series_order s (S b) ≠ ∞ → greatest_series_x_power K (series_stretch k s) (b * Pos.to_nat k)%nat = (Pos.to_nat k * greatest_series_x_power K s b)%nat.
proof: Proof. intros s b k Hinf. remember (greatest_series_x_power K s b) as m eqn:Hm . symmetry in Hm. apply greatest_series_x_power_iff. apply is_the_greatest_series_x_power_equiv. apply greatest_series_x_power_iff in Hm. remember (series_order s (S b)) as p eqn:Hp . symmetry in Hp. destruct p as [p| ]. apply series_order_stretch_succ with (k := k) in Hp. rewrite Hp. split. intros n. destruct Hm as (Hm, Hnm). unfold is_a_series_in_x_power in Hm. rewrite nth_series_order_stretch. apply Nat_divides_l. apply Nat.mod_divides. destruct m. assert (0 < 1)%nat as H by apply Nat.lt_0_1. apply Hnm in H. clear n. destruct H as (n, Hn). exfalso; apply Hn. exists (nth_series_order K s b n). rewrite Nat.mul_1_r; reflexivity. apply Nat.neq_mul_0; split; auto with Arith. pose proof (Hm n) as Hn. destruct Hn as (c, Hc). rewrite Hc. rewrite Nat.mul_assoc, Nat.mul_shuffle0. destruct m; [ rewrite Nat.mul_0_r; reflexivity | idtac ]. rewrite Nat.mul_comm. rewrite Nat.mod_mul; [ reflexivity | idtac ]. apply Nat.neq_mul_0; split; auto with Arith. intros u Hu. rewrite Nat.mul_comm, <- Nat.mul_assoc. destruct Hm as (Hm, Hmk). destruct m. exists O; simpl. rewrite Hp, Nat.mul_0_r. intros H. destruct H as (c, Hc). rewrite Nat.mul_0_r in Hc. discriminate Hc. assert (S m < S m * u)%nat as Hmu. apply mult_lt_compat_r with (p := S m) in Hu. rewrite Nat.mul_1_l, Nat.mul_comm in Hu. assumption. apply Nat.lt_0_succ. apply Hmk in Hmu. destruct Hmu as (n, Hn). exists n. intros H₁; apply Hn. rewrite nth_series_order_stretch in H₁. apply Nat.mod_divide in H₁. rewrite Nat.mul_mod_distr_l in H₁; auto with Arith. apply Nat.mul_eq_0_r in H₁; auto with Arith. apply Nat.mod_divide; auto with Arith. destruct u; [ exfalso; revert Hu; apply Nat.nlt_0_r | idtac ]. apply Nat.neq_mul_0; auto with Arith. destruct u; [ exfalso; revert Hu; apply Nat.nlt_0_r | idtac ]. apply Nat.neq_mul_0; auto with Arith. destruct u; [ exfalso; revert Hu; apply Nat.nlt_0_r | idtac ]. apply Nat.neq_mul_0; simpl; auto with Arith. exfalso; apply Hinf; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series