chore: migrate ByteArray.copyWithin to Lean core once lean#14158 lands

[kim-em]

This issue tracks removing the project-local ByteArray.copyWithin stopgap once the upstream Lean-core primitive lands and the toolchain bumps.

PR #2693 (closes #2675) shipped the single-pass back-reference copy via a temporary, owner-approved @[extern] exception to the no-@[extern] rule: a project-namespaced C symbol lean_zip_byte_array_copy_within (in c/copy_within_ffi.c) backing ByteArray.copyWithin (in Zip/Native/CopyWithin.lean), with reference body a ++ a.extract srcOff (srcOff + len). The core primitive is proposed in lean#14158 feat: add ByteArray.copyWithin.

When lean#14158 merges and the toolchain bumps:

• Delete c/copy_within_ffi.c and its lakefile target/extern_lib (copy_within_ffi.o, libcopy_within_ffi).
• Delete Zip/Native/CopyWithin.lean and drop the import Zip.Native.CopyWithin from Zip/Native/Inflate.lean.
• Use core's ByteArray.copyWithin directly. Core's @[extern "lean_byte_array_copy_within"] and identical reference body mean copyLoop's call site and the copyLoop_eq_ofFn proof (the one-line ByteArray.copyWithin unfold in Zip/Spec/DecodeCorrect.lean) stay unchanged.

The project-namespaced symbol was chosen specifically so the stopgap does not clash with core's lean_byte_array_copy_within across the bump.

🤖 Prepared with Claude Code