フィボナッチ数列の2通りの定義が等しいことを，Lean4 を使って証明する

Lean のコードスニペットを紹介します．テーマはフィボナッチ数列を計算する2通りのアルゴリズムが等しいことの検証です．

• 定義通りのフィボナッチ数列
• 高速化したフィボナッチ数列
• 両者が等しいことの証明

をそれぞれ Lean で実装したものです．