diff options
Diffstat (limited to 'theories/ZArith/Znat.v')
| -rw-r--r-- | theories/ZArith/Znat.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/ZArith/Znat.v b/theories/ZArith/Znat.v index d9bc4d1b2b..a0027efb33 100644 --- a/theories/ZArith/Znat.v +++ b/theories/ZArith/Znat.v @@ -97,7 +97,7 @@ intros x y H; rewrite H; trivial with arith. Qed. Theorem intro_Z : - forall n:nat, exists y : Z | Z_of_nat n = y /\ 0 <= y * 1 + 0. + forall n:nat, exists y : Z, Z_of_nat n = y /\ 0 <= y * 1 + 0. Proof. intros x; exists (Z_of_nat x); split; [ trivial with arith |