proposition: Theorem series_order_stretch_succ_inf : ∀ s n k, series_order s (S n) = ∞ → series_order (series_stretch k s) (S (n * Pos.to_nat k)) = ∞.
proof: Proof. intros s n k Hp. apply series_order_iff in Hp. apply series_order_iff. intros i. destruct (lt_dec (S i) (Pos.to_nat k)) as [H| H]. rewrite shifted_in_stretched; [ reflexivity | simpl ]. rewrite Nat.add_comm. rewrite <- Nat.add_succ_l. rewrite Nat.mod_add; [ idtac | apply Pos2Nat_ne_0 ]. rewrite Nat.mod_small; [ idtac | assumption ]. apply Nat.lt_0_succ. apply Nat.nlt_ge in H. rewrite Nat.add_succ_l, <- Nat.add_succ_r. eapply Nat.add_sub_assoc in H; symmetry in H. rewrite Nat.add_comm, Nat.add_sub in H; rewrite H. rewrite Nat.add_assoc, Nat.mul_comm. rewrite <- Nat.mul_succ_r, Nat.mul_comm. apply stretch_finite_series. assumption. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series