diff options
Diffstat (limited to 'theories/Numbers/Cyclic/Abstract/NZCyclic.v')
| -rw-r--r-- | theories/Numbers/Cyclic/Abstract/NZCyclic.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/Numbers/Cyclic/Abstract/NZCyclic.v b/theories/Numbers/Cyclic/Abstract/NZCyclic.v index 125fd3f12..589159390 100644 --- a/theories/Numbers/Cyclic/Abstract/NZCyclic.v +++ b/theories/Numbers/Cyclic/Abstract/NZCyclic.v @@ -17,9 +17,9 @@ Require Import CyclicAxioms. (** * From [CyclicType] to [NZAxiomsSig] *) -(** A [Z/nZ] representation given by a module type [CyclicType] - implements [NZAxiomsSig], e.g. the common properties between - N and Z with no ordering. Notice that the [n] in [Z/nZ] is +(** A [Z/nZ] representation given by a module type [CyclicType] + implements [NZAxiomsSig], e.g. the common properties between + N and Z with no ordering. Notice that the [n] in [Z/nZ] is a power of 2. *) @@ -98,7 +98,7 @@ Notation "x * y" := (NZmul x y) : IntScope. Theorem gt_wB_1 : 1 < wB. Proof. -unfold base. +unfold base. apply Zpower_gt_1; unfold Zlt; auto with zarith. Qed. |