diff options
Diffstat (limited to 'theories/Numbers/Natural/Abstract/NTimes.v')
| -rw-r--r-- | theories/Numbers/Natural/Abstract/NTimes.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/Numbers/Natural/Abstract/NTimes.v b/theories/Numbers/Natural/Abstract/NTimes.v index e15f02a1e..7d513dc46 100644 --- a/theories/Numbers/Natural/Abstract/NTimes.v +++ b/theories/Numbers/Natural/Abstract/NTimes.v @@ -52,7 +52,7 @@ Proof NZtimes_1_l. Theorem times_1_r : forall n : N, n * 1 == n. Proof NZtimes_1_r. -(** Theorems that cannot be proved in NZTimes *) +(* Theorems that cannot be proved in NZTimes *) (* In proving the correctness of the definition of multiplication on integers constructed from pairs of natural numbers, we'll need the |