Lean-Workbook Plus 39163: Trigonometric identity

Lean-Workbook Plus 39163: Fibonacci addition identity

For natural numbers $n,p$, $F_{n+p+1}=F_{n+1}F_{p+1}+F_nF_p$, where $F_0=0$, $F_1=1$ and $F_{j+2}=F_j+F_{j+1}$.

Source: Lean-Workbook row lean_workbook_plus_39163 (Apache-2.0). The unchanged proposition comes from the original record; its missing mathematical imports and namespaces are restored here.