diff options
| -rwxr-xr-x | theories/Bool/Zerob.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Bool/Zerob.v b/theories/Bool/Zerob.v index 6648ee6945..3c62e7ab07 100755 --- a/theories/Bool/Zerob.v +++ b/theories/Bool/Zerob.v @@ -21,6 +21,6 @@ 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). +Lemma zerob_false_elim : (n:nat)(zerob n)=false -> ~(n=O). Destruct n; [Intro H; Inversion H | Auto with bool]. Save. |