先生「1+1=2です」天才俺「なぜだ…」先生「いいから覚えろ」天才俺「なぜだ…納得しないと覚えられない…」

[29 以下、5ちゃんねるからVIPがお送りします 2023/07/03(月) 14:32:40.951 ID:eSXGnOT5H]

代数的データ型としてℕ︎をz∈ℕ︎, n∈ℕ︎⇒s(n)∈ℕ︎と定義して
+:ℕ︎→ℕ︎をwell-definedに定義してs(z)+s(z)=s(s(z))を示すだけ