proposition: Theorem series_order_stretch : ∀ s b k, series_order (series_stretch k s) (b * Pos.to_nat k) = (fin (Pos.to_nat k) * series_order s b)%Nbar.
proof: Proof. intros s b k. remember (series_order s b) as n eqn:Hn . symmetry in Hn. apply series_order_iff in Hn. apply series_order_iff. rewrite Nbar.mul_comm. destruct n as [n| ]; simpl. destruct Hn as (Hz, Hnz). split. intros i Hin. rewrite Nat.add_comm. rewrite Nat.mod_add; auto with Arith. rewrite Nat.div_add; auto with Arith. destruct (zerop (i mod Pos.to_nat k)) as [H₁| ]; [ idtac | reflexivity ]. apply Nat.mod_divides in H₁; [ idtac | apply Pos2Nat_ne_0 ]. destruct H₁ as (c, H₁). rewrite H₁. rewrite Nat.mul_comm. rewrite Nat.div_mul; auto with Arith. rewrite Nat.add_comm. apply Hz. rewrite H₁ in Hin. rewrite Nat.mul_comm in Hin. apply Nat.mul_lt_mono_pos_r in Hin; auto with Arith. rewrite <- Nat.mul_add_distr_r. rewrite Nat.mod_mul; auto with Arith; simpl. rewrite Nat.div_mul; auto with Arith. intros i. apply stretch_finite_series; assumption. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series