aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Numbers/NatInt/NZParity.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Numbers/NatInt/NZParity.v')
-rw-r--r--theories/Numbers/NatInt/NZParity.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/NatInt/NZParity.v b/theories/Numbers/NatInt/NZParity.v
index 0e9323789..1e6593b10 100644
--- a/theories/Numbers/NatInt/NZParity.v
+++ b/theories/Numbers/NatInt/NZParity.v
@@ -95,7 +95,7 @@ Proof.
intros.
generalize (Even_or_Odd n) (Even_Odd_False n).
rewrite <- even_spec, <- odd_spec.
- destruct (odd n), (even n); simpl; intuition.
+ destruct (odd n), (even n) ; simpl; intuition.
Qed.
Lemma negb_even : forall n, negb (even n) = odd n.