blob: 3c62e7ab0734377216bac102400f1a3e7ba210af (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
|
(* $Id$ *)
Require Arith.
Require Bool.
Definition zerob : nat->bool
:= [n:nat]Cases n of O => true | (S _) => false end.
Lemma zerob_true_intro : (n:nat)(n=O)->(zerob n)=true.
Destruct n; [Trivial with bool | Intros p H; Inversion H].
Save.
Hints Resolve zerob_true_intro : bool.
Lemma zerob_true_elim : (n:nat)(zerob n)=true->(n=O).
Destruct n; [Trivial with bool | Intros p H; Inversion H].
Save.
Lemma zerob_false_intro : (n:nat)~(n=O)->(zerob n)=false.
Destruct n; [Destruct 1; Auto with bool | Trivial with bool].
Save.
Hints Resolve zerob_false_intro : bool.
Lemma zerob_false_elim : (n:nat)(zerob n)=false -> ~(n=O).
Destruct n; [Intro H; Inversion H | Auto with bool].
Save.
|
