Lean-Workbook Syntax 61921: A sum of squared Fibonacci numbers

For every natural $n$, $\sum_{k=0}^{n}F_k^2=F_nF_{n+1}$, where $F_0=0,F_1=1$ and $F_{n+2}=F_{n+1}+F_n$.

Source: Lean-Workbook row lean_workbook_plus_61921 (Apache-2.0), original record. This corrected declaration replaces the obsolete finite sum/product binder in with ∈ and restores required imports or namespaces. Ranges, casts, quantifiers, and mathematical expressions are preserved.