Does every n admit a k with the product of k consecutive integers from n dividing the next k? (Erdős #389)

This is a question of Erdős and Straus. For an integer $n\geq 1$, is there always a positive integer $k$ such that the product of the $k$ consecutive integers starting at $n$ divides the product of the next $k$ consecutive integers, i.e. $$n(n+1)\cdots(n+k-1)\mid (n+k)(n+k+1)\cdots(n+2k-1)?$$ For example, $n=2$ works with $k=5$, since $2\cdot 3\cdot 4\cdot 5\cdot 6=720$ divides $7\cdot 8\cdot 9\cdot 10\cdot 11=55440$; and $n=3$ works with $k=4$, since $3\cdot 4\cdot 5\cdot 6=360$ divides $7\cdot 8\cdot 9\cdot 10=5040$. The question is whether such a $k$ exists for every $n$.

Acceptance. FULLY RESOLVES: a proof (machine-checkable in Lean/Coq preferred, matching the existing formalisation, otherwise a complete written proof) that for every $n\geq 1$ there exists $k$ with $n(n+1)\cdots(n+k-1)\mid(n+k)\cdots(n+2k-1)$; OR a specific $n$ together with a genuine impossibility proof that no $k$ works for it (no finite computation alone can certify non-existence). ADVANCES: (a) extend OEIS A375071 by computing the least valid $k$ for new values of $n$ beyond $n=18$, delivered with the search program and the verified divisibility certificates; (b) prove existence of a valid $k$ for an infinite explicitly-described family of $n$ (e.g. all $n$ in a fixed congruence class, or all primes $n$), with proof; (c) establish a nontrivial upper bound on the least valid $k$ as a function of $n$, with proof. Deliver the extended sequence plus code, or the proof file.