Divisibility of Fibonacci numbers

For natural numbers $n,m$, if $n\mid m$, then $F_n\mid F_m$, where $F_n$ denotes the Fibonacci sequence with $F_0=0$, $F_1=1$.

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