Library Coq.Bool.Zerob
Require
Import
Arith
.
Require
Import
Bool
.
Open
Local
Scope
nat_scope
.
Definition
zerob
(
n
:nat) :
bool
:=
match
n
with
|
O
=>
true
|
S
_
=>
false
end
.
Lemma
zerob_true_intro
:
forall
n
:nat,
n
= 0 ->
zerob
n
=
true
.
Hint
Resolve
zerob_true_intro
:
bool
.
Lemma
zerob_true_elim
:
forall
n
:nat,
zerob
n
=
true
->
n
= 0.
Lemma
zerob_false_intro
:
forall
n
:nat,
n
<> 0 ->
zerob
n
=
false
.
Hint
Resolve
zerob_false_intro
:
bool
.
Lemma
zerob_false_elim
:
forall
n
:nat,
zerob
n
=
false
->
n
<> 0.