- 63 名前：デフォルトの名無しさん mailto:sage [2011/07/13(水) 23:22:33.05 ]
- Require Import Classical.
Theorem eom : forall P:Prop, P \/ ~P.
intro P.
apply NNPP.
intro H.
elim H.
right.
intro p.
elim H.
left.
assumption.
Qed.
こんな知ってるか知らないかだし
CoqIDEなるProofGEneralなり使って一行ずつ動かしながらどうGoalが変化するか観察するのがいいよ
俺はそうやって覚えた
