- 11/24 [Schedule/ProofCafe_25]()
- 時間: 14:30 - 17:30
- 場所: 名古屋大学 理学部1号館 409
- 参加登録: [PARTAKE: ProofCafe](http://partake.in/events/1324956f-30dc-401a-964b-e80a6478f5ca)
- [ソフトウェアの基礎](http://proofcafe.org/sf/)の[命題と論拠](http://proofcafe.org/sf/Prop_J.html)の「???」から
- ドキュメントはCoqソースコードから自動生成されています。ソースコード全体はこちら: [http://proofcafe.org/sf/sfja.tar.gz]()


加者 6人

## 練習問題:  ★★ (not_eq_beq_false)
~~~ { .v }
Require Import Arith.

Theorem not_eq_beq_false : forall n n' : nat,
     n <> n' ->
     beq_nat n n' = false.
Proof.
  induction n; destruct n'; simpl; intros; try reflexivity.
  induction H; reflexivity.
  apply IHn.
  intro H'; rewrite H' in *; apply H.
  reflexivity.
Qed.  
~~~