自分が中二レベルであることを証明する - ろじかるんるんものがたり旧聞になりますが「大学生の４人に１人「平均」分からず 数学基本調査、論理力欠如明確に」より引用。 「偶数に奇数を足すと必ず奇数になる」ことを数式と文章で説明する中２レベルの問題 ということらしいので coq を使って自分が中二レベルあることを証明してみましょう！ まずは奇数とは、偶数とは何なのかを帰納的に定義してやりましょう。 Inductive even : nat -> Prop := | even_O : even 0 | even_S : forall n, odd n -> even (S n) with odd : nat -> Prop := | odd_S : forall n, even n -> odd (S n). 見たままですね。証明したい定理はこんな感じじゃないでしょうか。 Theorem odd_plus_l : forall n m, odd n -> eve
