15/01/16 00:10:36.55 tbQRRWp6.net
できたっぽい。
片山さんに教えてもらったページみた。
Require Import Even.
Theorem t:forall n:nat,even (n * (1+n)).
intros.
apply even_mult_aux.
elim n.
left.
apply even_O.
intros.
elim H.
right.
apply even_S.
apply odd_S.
apply H0.
left.
apply H0.
Qed.
Coq相当親切なチュートリアルがないと勉強できんわ。
どのタクティク使えばいいのかとかわからんすぎる。