>>568 説明ありがとうございます。
たしかに直感的にはわかりやすい証明？ですね。
無限を無限によって定義するという、どうどうめぐりの定義が
可能なhaskellではこの証明法けっこう応用できそうな気がします。

まともな数学教育受けてないので、余帰納法とかわかりませんが、
それの説明は難しそうですね。

出典は
Introduction Functional Programming using Haskell
second edition by Richard Bird
p67
3.2.1. Full Induction
...If we want to show that a property P also holds for every
partial number, then we have to prove three things:
Case(U). That P(U) holds. （UはTのさかさまのかわり）
Case(Zero). That P(Zero) holds.
Case(Succ n). That if P(n) holds, then P(Succ n)　holds also.
We can omit the second case, but then we can conclude only
that P(n) holds for every partial number. The reason the
principle is valid is that every partial number is either U or
of the form Succ n for some partial number n. .....