proposition: Theorem shifted_in_stretched : ∀ s k i, (0 < i mod Pos.to_nat k)%nat → (series_stretch k s) .[i] = 0%K.
proof: Proof. intros s k i Hi; simpl. destruct (zerop (i mod Pos.to_nat k)) as [Hz| ]; [ idtac | reflexivity ]. exfalso; revert Hi; rewrite Hz; apply Nat.lt_irrefl. Qed.
imports: Utf8 QArith NPeano Misc NbarM Field2 Power_series