proposition: Theorem series_stretch_shrink : ∀ s k, (Pos.to_nat k | greatest_series_x_power K s 0) → (series_stretch k (series_shrink k s) = s)%ser.
proof: Proof. intros s k Hk. constructor; intros i; simpl. destruct (zerop (i mod Pos.to_nat k)) as [H₁| H₁]. apply Nat.mod_divides in H₁; auto with Arith. destruct H₁ as (c, Hc); rewrite Nat.mul_comm in Hc; subst i. rewrite Nat.div_mul; auto with Arith; reflexivity. destruct Hk as (c, Hk). apply greatest_series_x_power_iff in Hk. remember (series_order s 1) as p eqn:Hp . symmetry in Hp. destruct p as [p| ]. destruct Hk as (Hz, Hnz). symmetry. destruct c. simpl in Hz. unfold is_a_series_in_x_power in Hz. pose proof (Hz 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 (i mod (S c * Pos.to_nat k) ≠ 0)%nat as H. intros H. apply Nat.mod_divides in H. destruct H as (d, Hd). rewrite Nat.mul_shuffle0 in Hd. rewrite Hd in H₁. rewrite Nat.mod_mul in H₁; auto with Arith. revert H₁; apply Nat.lt_irrefl. apply Nat.neq_mul_0. split; auto with Arith. remember (S c) as d eqn:Hd . rewrite <- Nat2Pos.id in Hd; auto; subst d. rewrite <- Pos2Nat.inj_mul in H. rewrite <- Pos2Nat.inj_mul in Hz. eapply series_nth_0_in_interval in H; eassumption. symmetry. apply series_order_iff in Hp. simpl in Hp. destruct i; [ idtac | apply Hp ]. rewrite Nat.mod_0_l in H₁; auto with Arith. exfalso; revert H₁; apply Nat.lt_irrefl. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series