diff options
Diffstat (limited to 'theories/NArith/Pnat.v')
| -rw-r--r-- | theories/NArith/Pnat.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/NArith/Pnat.v b/theories/NArith/Pnat.v index c0e2bb020f..11410c7899 100644 --- a/theories/NArith/Pnat.v +++ b/theories/NArith/Pnat.v @@ -124,7 +124,7 @@ Qed. (** [nat_of_P] maps to the strictly positive subset of [nat] *) -Lemma ZL4 : forall p:positive, exists h : nat | nat_of_P p = S h. +Lemma ZL4 : forall p:positive, exists h : nat, nat_of_P p = S h. Proof. intro y; induction y as [p H| p H| ]; [ destruct H as [x H1]; exists (S x + S x); unfold nat_of_P in |- *; |