aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Bool/Zerob.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Bool/Zerob.v')
-rw-r--r--theories/Bool/Zerob.v16
1 files changed, 10 insertions, 6 deletions
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v
index eac13569a..5e9d4afa6 100644
--- a/theories/Bool/Zerob.v
+++ b/theories/Bool/Zerob.v
@@ -15,24 +15,28 @@ Open Local Scope nat_scope.
Definition zerob (n:nat) : bool :=
match n with
- | O => true
- | S _ => false
+ | O => true
+ | S _ => false
end.
Lemma zerob_true_intro : forall n:nat, n = 0 -> zerob n = true.
-destruct n; [ trivial with bool | inversion 1 ].
+Proof.
+ destruct n; [ trivial with bool | inversion 1 ].
Qed.
Hint Resolve zerob_true_intro: bool.
Lemma zerob_true_elim : forall n:nat, zerob n = true -> n = 0.
-destruct n; [ trivial with bool | inversion 1 ].
+Proof.
+ destruct n; [ trivial with bool | inversion 1 ].
Qed.
Lemma zerob_false_intro : forall n:nat, n <> 0 -> zerob n = false.
-destruct n; [ destruct 1; auto with bool | trivial with bool ].
+Proof.
+ destruct n; [ destruct 1; auto with bool | trivial with bool ].
Qed.
Hint Resolve zerob_false_intro: bool.
Lemma zerob_false_elim : forall n:nat, zerob n = false -> n <> 0.
-destruct n; [ intro H; inversion H | auto with bool ].
+Proof.
+ destruct n; [ inversion 1 | auto with bool ].
Qed. \ No newline at end of file