豊福です。

  いっぱい反応したいですが、とっても余裕が
ないのでつっこみだけ。

ごとけんさん [ruby-math:00012]
> 上の等号をもし証明ぽく示すなら、
>   succ**n(m) => succ**n(succ**m(0))
  ...
>              => succ(succ(...(succ(succ(succ(...succ(0)...))))...))
>                 |<-- succがn個 -->|<-- succがm個 -->|

    succ**m(n) => succ(succ(...(succ(succ(succ(...succ(0)...))))...))
                  |<-- succがm個 -->|<-- succがn個 -->|

  これだと「n個の後にm個」と「m個の後にn個」が
等しいかということになって n+m == m+n かという
問題に戻ってしまいませんか。
証明っぽくするには数学的帰納法かな。
---
                        豊福
                        toyofuku / juice.or.jp