proposition: Theorem stretch_finite_series : ∀ s b k, (∀ i, (s .[b + i] = 0)%K) → ∀ i, ((series_stretch k s) .[b * Pos.to_nat k + i] = 0)%K.
proof: Proof. intros s b k Hz i. destruct (zerop (i mod Pos.to_nat k)) as [H₁| H₁]. apply Nat.mod_divides in H₁; [ idtac | apply Pos2Nat_ne_0 ]. destruct H₁ as (c, H₁). subst i. rewrite Nat.mul_comm, <- Nat.mul_add_distr_l. rewrite series_nth_mul_stretch. apply Hz. rewrite shifted_in_stretched; [ reflexivity | idtac ]. rewrite Nat.add_comm. rewrite Nat.mod_add; [ assumption | apply Pos2Nat_ne_0 ]. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series